Theorem 19.23t

Closed form of Theorem 19.23 of [Margaris] p. 90. See 19.23. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) [df-nf] changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 8-Oct-2022.)

Conclusion
\( \vdash \Finv x \, \psi \rightarrow (\forall x \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \psi) \)
Proof
l0
19.38b
\( \vdash \Finv x \, \psi \rightarrow (\exists x \, \varphi \rightarrow \forall x \, \psi \leftrightarrow \forall x \, (\varphi \rightarrow \psi)) \)
19.3t
imbi2d _
\( \vdash \Finv x \, \psi \rightarrow (\exists x \, \varphi \rightarrow \forall x \, \psi \leftrightarrow \exists x \, \varphi \rightarrow \psi) \)
bitr3d l0 _