Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁ (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 := MP s1 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 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'

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 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 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'

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:
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