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

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

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

State before:
case a
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ Γ) (P.imp_ Q)
Tactic:
apply T_14_10_comm
State after:
case a.h1
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ (P.imp_ Q)

State before:
case a.h1
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Γ (P.imp_ Q)
Tactic:
exact h2
State after:
no goals

State before:
case a
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct (Δ ∪ Γ) P
Tactic:
apply T_14_10
State after:
case a.h1
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Δ P

State before:
case a.h1
P Q : Formula
Δ Γ : Set Formula
h1 : IsDeduct Δ P
h2 : IsDeduct Γ (P.imp_ Q)
⊢ IsDeduct Δ P
Tactic:
exact h1
State after:
no goals