Theorem 19.2d

Deduction associated with 19.2. (Contributed by BJ, 12-May-2019.)

Hypothesis
19.2d.1
\( \vdash \varphi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \)
Proof
l0
19.2d.1
\( \vdash \varphi \rightarrow \forall x \, \psi \)
19.2
\( \vdash \forall x \, \psi \rightarrow \exists x \, \psi \)
syl l0 _