Theorem 19.36v

Version of 19.36 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.)

Conclusion
\( \vdash \exists x \, (\varphi \rightarrow \psi) \leftrightarrow \forall x \, \varphi \rightarrow \psi \)
Proof
l0
19.35
\( \vdash \exists x \, (\varphi \rightarrow \psi) \leftrightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
19.9v
imbi2i _
\( \vdash \forall x \, \varphi \rightarrow \exists x \, \psi \leftrightarrow \forall x \, \varphi \rightarrow \psi \)
bitri l0 _