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

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

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

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

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

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

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

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

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

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

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

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