apply IsDeduct.mp_ (P.imp_ (h1_phi.imp_ h1_psi))
case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi))
case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))

case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))