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

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

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

case a
P : Formula
⊢ IsDeduct ∅ (P.not_.not_.not_.imp_ P.not_)

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

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

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

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