Theorem 19.37imv

One direction of 19.37v that can be proven without [ax-6]. (Contributed by Rohan Ridenour, 16-Apr-2022.)

Conclusion
\( \vdash \exists x \, (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \exists x \, \psi \)
Proof
l0
ax-5
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
19.35
biimpi _
\( \vdash \exists x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
syl5 l0 _