Theorem: PropositionalLogic.HilbertSystem.HPM.disjComm (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 : {φ ∨' ψ} ⊢ φ →' (ψ ∨' φ) := by apply axiomIDisj₂;
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 : {φ ∨' ψ} ⊢ ψ →' (ψ ∨' φ) := by apply axiomIDisj₁;
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 s5 := MP (EDisj s2 s3) 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 : {φ ∨' ψ} ⊢ ψ →' ψ ∨' φ
s5 : {φ ∨' ψ} ⊢ ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ

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 : {φ ∨' ψ} ⊢ ψ →' ψ ∨' φ
s5 : {φ ∨' ψ} ⊢ ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ ∨' φ
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

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:
apply axiomIDisj₂
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
s1 : {φ ∨' ψ} ⊢ φ ∨' ψ
s2 : {φ ∨' ψ} ⊢ φ →' ψ ∨' φ
⊢ {φ ∨' ψ} ⊢ ψ →' ψ ∨' φ
Tactic:
apply axiomIDisj₁
State after:
no goals