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

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

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

State before:
case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ {P}) (P.imp_ Q)
Tactic:
exact T_14_10 (P.imp_ Q) Δ h1 {P}
State after:
no goals

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

State before:
case a.a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ (P.imp_ Q)
⊢ P ∈ Δ ∪ {P}
Tactic:
simp
State after:
no goals