Theorem: PropositionalLogic.HilbertSystem.HPM.conjCommLiff (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 [ conjComm]
State after:
no goals