awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₁₈ : c → b → a → b → a → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₁₉ : c → b → a → b → c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₂₀ : ¬c → ¬a → b → a → c → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₂₉ : ¬c → b → ¬a → b → a → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mp₃₀ : ¬c → b → ¬a → b → c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₉ : b → a → c → a → b → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₁₀ : b → a → c → ¬a → ¬b → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₁₁ : b → ¬a → ¬c → a → b → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₁₅ : b → c → a → c → (a ↔ b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₁₈ : b → c → a → c → a → b
Tactic: tauto