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