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)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₁₂ : b → a → a → c → b → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₁₃ : b → a → a → c → c → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₁₄ : b → a → c → b → c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₁₅ : b → a → c → ¬b → ¬c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₁₆ : b → ¬a → ¬c → b → c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₂₁ : ¬b → a → ¬¬a → ¬c → (b ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
mpr₂₁ mpr₂₂ : ¬b → a → ¬¬a → ¬c → (b ↔ c)
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₂₃ : ¬b → a → ¬¬a → ¬c → b → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
mpr₂₁ mpr₂₂ : ¬b → a → ¬¬a → ¬c → (b ↔ c)
mpr₂₃ : ¬b → a → ¬¬a → ¬c → b → c
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₂₄ : ¬b → a → ¬¬a → ¬c → c → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
mpr₂₁ mpr₂₂ : ¬b → a → ¬¬a → ¬c → (b ↔ c)
mpr₂₃ : ¬b → a → ¬¬a → ¬c → b → c
mpr₂₄ : ¬b → a → ¬¬a → ¬c → c → b
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₂₅ : ¬b → ¬a → c → b → c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
mpr₂₁ mpr₂₂ : ¬b → a → ¬¬a → ¬c → (b ↔ c)
mpr₂₃ : ¬b → a → ¬¬a → ¬c → b → c
mpr₂₄ : ¬b → a → ¬¬a → ¬c → c → b
mpr₂₅ : ¬b → ¬a → c → b → c → a
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₂₆ : ¬b → ¬a → c → ¬b → ¬c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
mpr₂₁ mpr₂₂ : ¬b → a → ¬¬a → ¬c → (b ↔ c)
mpr₂₃ : ¬b → a → ¬¬a → ¬c → b → c
mpr₂₄ : ¬b → a → ¬¬a → ¬c → c → b
mpr₂₅ : ¬b → ¬a → c → b → c → a
mpr₂₆ : ¬b → ¬a → c → ¬b → ¬c → a
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₂₇ : ¬b → ¬¬a → ¬c → b → c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
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₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
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₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
mpr₂₁ mpr₂₂ : ¬b → a → ¬¬a → ¬c → (b ↔ c)
mpr₂₃ : ¬b → a → ¬¬a → ¬c → b → c
mpr₂₄ : ¬b → a → ¬¬a → ¬c → c → b
mpr₂₅ : ¬b → ¬a → c → b → c → a
mpr₂₆ : ¬b → ¬a → c → ¬b → ¬c → a
mpr₂₇ : ¬b → ¬¬a → ¬c → b → c → a
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₂₈ : ¬b → ¬¬a → ¬c → ¬b → ¬c → a
Tactic: tauto