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