Theorem nfnth

Description: 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)

	Ref	Expression
Hypothesis	nfnth.1	$$⊢\neg \phi$$
Assertion	nfnth	$$⊢Ⅎx\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfnth.1	$$⊢\neg \phi$$
2		nfntht2	$$⊢\forall x\neg \phi \to Ⅎx\phi$$
3	2 1	mpg	$$⊢Ⅎx\phi$$