apply IsDeduct.mp_ (exists_ v P)
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ Q
case a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ ((exists_ v P).imp_ Q)

case a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (exists_ v P)