induction h1
P Q : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {P}) Q
⊢ IsDeduct Δ (P.imp_ Q)
case axiom_
P Q : Formula
Δ : Set Formula
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ (P.imp_ phi✝)

case assume_
P Q : Formula
Δ : Set Formula
phi✝ : Formula
a✝ : phi✝ ∈ Δ ∪ {P}
⊢ IsDeduct Δ (P.imp_ phi✝)

case mp_
P Q : Formula
Δ : Set Formula
phi✝ psi✝ : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (phi✝.imp_ psi✝)
a✝ : IsDeduct (Δ ∪ {P}) phi✝
a_ih✝¹ : IsDeduct Δ (P.imp_ (phi✝.imp_ psi✝))
a_ih✝ : IsDeduct Δ (P.imp_ phi✝)
⊢ IsDeduct Δ (P.imp_ psi✝)