Theorem: PropositionalLogic.HilbertSystem.HPM₀.DNI (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 s2 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 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'

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