apply IsDeduct.mp_ P
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsDeduct Δ Q
case a
P Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
h2 : IsProof (P.imp_ Q)
⊢ IsDeduct Δ (P.imp_ Q)

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