Theorem nfnth

No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016.) [df-nf] changed. (Revised by Wolf Lammen, 12-Sep-2021.)

Hypothesis
nfnth.1
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \Finv x \, \varphi \)
Proof
l0
nfntht2
\( \vdash \forall x \, \neg \varphi \rightarrow \Finv x \, \varphi \)
nfnth.1
\( \vdash \neg \varphi \)
mpg l0 _