apply IsDeduct.mp_ h1_phi
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (P.imp_ h1_phi)
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))

case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi