Theorem: PropositionalLogic.HilbertSystem.HPM.disjCommLiff (PropositionalLogic/HilbertSystem/HPM.lean)

State before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ φ ∨' ψ ↔' ψ ∨' φ
Tactic:
apply ILiff'
State after:
case a
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ (∅ ⊢ φ ∨' ψ →' ψ ∨' φ) ∧ (∅ ⊢ ψ ∨' φ →' φ ∨' ψ)

State before:
case a
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ (∅ ⊢ φ ∨' ψ →' ψ ∨' φ) ∧ (∅ ⊢ ψ ∨' φ →' φ ∨' ψ)
Tactic:
apply And.intro <;> simp [ disjComm]
State after:
no goals