Theorem 19.23v

Version of 19.23 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) Remove dependency on [ax-6]. (Revised by Rohan Ridenour, 15-Apr-2022.)

Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \psi \)
Proof
l0
exim
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists x \, \varphi \rightarrow \exists x \, \psi \)
ax5e
\( \vdash \exists x \, \psi \rightarrow \psi \)
l2
syl6 l0 _
ax-5
l4
imim2i _
\( \vdash (\exists x \, \varphi \rightarrow \psi) \rightarrow \exists x \, \varphi \rightarrow \forall x \, \psi \)
19.38
\( \vdash (\exists x \, \varphi \rightarrow \forall x \, \psi) \rightarrow \forall x \, (\varphi \rightarrow \psi) \)
syl l4 _
impbii l2 _