Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp' (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
φ : L
⊢ ∅ ⊢ φ →' φ
Tactic:
have s1 : ⊢ (φ →' (φ →' φ) →' φ) := by apply axiomK;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ 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
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
⊢ ∅ ⊢ φ →' φ
Tactic:
have s2 : ⊢ ((φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ) := by apply axiomS;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ 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
φ : 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
φ : 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
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
⊢ ∅ ⊢ φ →' φ
Tactic:
have s4 : ⊢ (φ →' φ →' φ) := by apply axiomK;
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ 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
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
s4 : ∅ ⊢ φ →' φ →' φ
⊢ ∅ ⊢ φ →' φ
Tactic:
have s5 : ⊢ (φ →' φ) := MP s3 s4
State after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ 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
φ : 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
φ : L
⊢ ∅ ⊢ φ →' (φ →' φ) →' φ
Tactic:
apply axiomK
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
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
⊢ ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
Tactic:
apply axiomS
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
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
⊢ ∅ ⊢ φ →' φ →' φ
Tactic:
apply axiomK
State after:
no goals