Theorem 19.23h

Theorem 19.23 of [Margaris] p. 90. See 19.23. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)

Hypothesis
19.23h.1
\( \vdash \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \psi \)
Proof
19.23h.1
nf5i _
19.23 _