Theorem 19.8ad

If a wff is true, it is true for at least one instance. Deduction form of 19.8a. (Contributed by DAW, 13-Feb-2017.)

Hypothesis
19.8ad.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \)
Proof
l0
19.8ad.1
\( \vdash \varphi \rightarrow \psi \)
19.8a
\( \vdash \psi \rightarrow \exists x \, \psi \)
syl l0 _