Theorem 19.36imv

One direction of 19.36v that can be proven without [ax-6]. (Contributed by Rohan Ridenour, 16-Apr-2022.) (Proof shortened by Wolf Lammen, 22-Sep-2024.)

Conclusion
\( \vdash \exists x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \psi \)
Proof
pm2.27
l1
aleximi _
\( \vdash \forall x \, \varphi \rightarrow \exists x \, (\varphi \rightarrow \psi) \rightarrow \exists x \, \psi \)
ax5e
\( \vdash \exists x \, \psi \rightarrow \psi \)
syl6com l1 _