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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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