Theorem 19.37iv

Inference associated with 19.37v. (Contributed by NM, 5-Aug-1993.) Remove dependency on [ax-6]. (Revised by Rohan Ridenour, 15-Apr-2022.)

Hypothesis
19.37iv.1
\( \vdash \exists x \, (\varphi \rightarrow \psi) \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \)
Proof
l0
19.37iv.1
\( \vdash \exists x \, (\varphi \rightarrow \psi) \)
19.37imv
\( \vdash \exists x \, (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \exists x \, \psi \)
ax-mp l0 _