Theorem nfal

Description: If x is not free in ph , then it is not free in A. y ph . (Contributed by Mario Carneiro, 11-Aug-2016)

	Ref	Expression
Hypothesis	nfal.1	$$⊢Ⅎx\phi$$
Assertion	nfal	$$⊢Ⅎx\forall y\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfal.1	$$⊢Ⅎx\phi$$
2	1	nf5ri	$$⊢\phi \to \forall x\phi$$
3	2	hbal	$$⊢\forall y\phi \to \forall x\forall y\phi$$
4	3	nf5i	$$⊢Ⅎx\forall y\phi$$