Theorem 19.35

Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)

Conclusion
\( \vdash \exists x \, (\varphi \rightarrow \psi) \leftrightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
Proof
pm2.27
aleximi _
l2
com12 _
l3
exnal
\( \vdash \exists x \, \neg \varphi \leftrightarrow \neg \forall x \, \varphi \)
pm2.21
eximi _
\( \vdash \exists x \, \neg \varphi \rightarrow \exists x \, (\varphi \rightarrow \psi) \)
l6
sylbir l3 _
exa1
ja l6 _
impbii l2 _