Theorem: FOL.NV.T_14_5 (FOL/NV/Margaris/Prop.lean)

State before:
P : Formula
⊢ IsProof (P.not_.not_.imp_ P)
Tactic:
simp only [IsProof]
State after:
P : Formula
⊢ IsDeduct ∅ (P.not_.not_.imp_ P)

State before:
P : Formula
⊢ IsDeduct ∅ (P.not_.not_.imp_ P)
Tactic:
apply deduction_theorem
State after:
case h1
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P

State before:
case h1
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P
Tactic:
apply IsDeduct.mp_ P.not_.not_
State after:
case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ P)

case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_

State before:
case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ P)
Tactic:
apply IsDeduct.mp_ (P.not_.imp_ P.not_.not_.not_)
State after:
case h1.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) ((P.not_.imp_ P.not_.not_.not_).imp_ (P.not_.not_.imp_ P))

case h1.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.imp_ P.not_.not_.not_)

State before:
case h1.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) ((P.not_.imp_ P.not_.not_.not_).imp_ (P.not_.not_.imp_ P))
Tactic:
apply IsDeduct.axiom_
State after:
case h1.a.a.a
P : Formula
⊢ IsAxiom ((P.not_.imp_ P.not_.not_.not_).imp_ (P.not_.not_.imp_ P))

State before:
case h1.a.a.a
P : Formula
⊢ IsAxiom ((P.not_.imp_ P.not_.not_.not_).imp_ (P.not_.not_.imp_ P))
Tactic:
apply IsAxiom.prop_3_
State after:
no goals

State before:
case h1.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.imp_ P.not_.not_.not_)
Tactic:
apply IsDeduct.mp_ P.not_.not_
State after:
case h1.a.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ (P.not_.imp_ P.not_.not_.not_))

case h1.a.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_

State before:
case h1.a.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ (P.not_.imp_ P.not_.not_.not_))
Tactic:
apply proof_imp_deduct
State after:
case h1.a.a.a.h1
P : Formula
⊢ IsProof (P.not_.not_.imp_ (P.not_.imp_ P.not_.not_.not_))

State before:
case h1.a.a.a.h1
P : Formula
⊢ IsProof (P.not_.not_.imp_ (P.not_.imp_ P.not_.not_.not_))
Tactic:
apply T_13_6
State after:
no goals

State before:
case h1.a.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.a.a.a
P : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.not_.not_}

State before:
case h1.a.a.a.a
P : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.not_.not_}
Tactic:
simp
State after:
no goals

State before:
case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.a
P : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.not_.not_}

State before:
case h1.a.a
P : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.not_.not_}
Tactic:
simp
State after:
no goals