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

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

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

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

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

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

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

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

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

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

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

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

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