Theorem 19.23

Theorem 19.23 of [Margaris] p. 90. See 19.23v for a version requiring fewer axioms. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Hypothesis
19.23.1
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \psi \)
Proof
l0
19.23.1
\( \vdash \Finv x \, \psi \)
19.23t
\( \vdash \Finv x \, \psi \rightarrow (\forall x \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \psi) \)
ax-mp l0 _