Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂ (PropositionalLogic/HilbertSystem/HPM₀.lean)

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ⊢ (φ →' ¬'ψ) →' ψ →' ¬'φ
Tactic:
simp [deduction]
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ := by simp;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ := by simp;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥' := by simp;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s4 := MP s3 s1
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s5 := MP s4 s2
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ →' ⊥'
s5 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ →' ⊥'
s5 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
assumption
State after:
no goals

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
Tactic:
simp
State after:
no goals

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
Tactic:
simp
State after:
no goals

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
Tactic:
simp
State after:
no goals