Theorem 19.21t

Closed form of Theorem 19.21 of [Margaris] p. 90, see 19.21. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) [df-nf] changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 3-Nov-2021.)

Conclusion
\( \vdash \Finv x \, \varphi \rightarrow (\forall x \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, \psi) \)
Proof
l0
19.38a
\( \vdash \Finv x \, \varphi \rightarrow (\exists x \, \varphi \rightarrow \forall x \, \psi \leftrightarrow \forall x \, (\varphi \rightarrow \psi)) \)
19.9t
imbi1d _
\( \vdash \Finv x \, \varphi \rightarrow (\exists x \, \varphi \rightarrow \forall x \, \psi \leftrightarrow \varphi \rightarrow \forall x \, \psi) \)
bitr3d l0 _