Theorem nfntht2

Closed form of nfnth. (Contributed by BJ, 16-Sep-2021.) (Proof shortened by Wolf Lammen, 4-Sep-2022.)

Conclusion
\( \vdash \forall x \, \neg \varphi \rightarrow \Finv x \, \varphi \)
Proof
l0
alnex
\( \vdash \forall x \, \neg \varphi \leftrightarrow \neg \exists x \, \varphi \)
nfntht
\( \vdash \neg \exists x \, \varphi \rightarrow \Finv x \, \varphi \)
sylbi l0 _