Theorem nfth

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

Hypothesis
nfth.1
\( \vdash \varphi \)
Conclusion
\( \vdash \Finv x \, \varphi \)
Proof
l0
nftht
\( \vdash \forall x \, \varphi \rightarrow \Finv x \, \varphi \)
nfth.1
\( \vdash \varphi \)
mpg l0 _