Theorem 19.38

Theorem 19.38 of [Margaris] p. 90. The converse holds under nonfreeness conditions, see 19.38a and 19.38b. (Contributed by NM, 12-Mar-1993.) Allow a shortening of 19.21t. (Revised by Wolf Lammen, 2-Jan-2018.)

Conclusion
\( \vdash (\exists x \, \varphi \rightarrow \forall x \, \psi) \rightarrow \forall x \, (\varphi \rightarrow \psi) \)
Proof
l0
alnex
\( \vdash \forall x \, \neg \varphi \leftrightarrow \neg \exists x \, \varphi \)
pm2.21
alimi _
\( \vdash \forall x \, \neg \varphi \rightarrow \forall x \, (\varphi \rightarrow \psi) \)
l3
sylbir l0 _
ala1
ja l3 _