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

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

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

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

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

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

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

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

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

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

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

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

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

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