Theorem: PropositionalLogic.HilbertSystem.HPM.conjComm (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:
simp [deduction]
State after:
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:
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:
have s1 : {φ ∧' ψ} ⊢ φ ∧' ψ := by simp;
State after:
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
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ

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
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
have s2 := EConj₂ s1
State after:
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
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ

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
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
have s3 := EConj₁ s1
State after:
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
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
s3 : {φ ∧' ψ} ⊢ φ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ

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
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
s3 : {φ ∧' ψ} ⊢ φ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
have s6 := IConj s2 s3
State after:
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
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
s3 : {φ ∧' ψ} ⊢ φ
s6 : {φ ∧' ψ} ⊢ ψ ∧' φ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ

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
s1 : {φ ∧' ψ} ⊢ φ ∧' ψ
s2 : {φ ∧' ψ} ⊢ ψ
s3 : {φ ∧' ψ} ⊢ φ
s6 : {φ ∧' ψ} ⊢ ψ ∧' φ
⊢ {φ ∧' ψ} ⊢ ψ ∧' φ
Tactic:
assumption
State after:
no goals

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:
simp
State after:
no goals