Theorem nfth

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

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

Proof

Step	Hyp	Ref	Expression
1		nfth.1	$$⊢\phi$$
2		nftht	$$⊢\forall x\phi \to Ⅎx\phi$$
3	2 1	mpg	$$⊢Ⅎx\phi$$