Theorem nfal

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

	Ref	Expression
Hypothesis	nfal.1	⊢ Ⅎ 𝑥 𝜑
Assertion	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 𝜑

Proof

Step	Hyp	Ref	Expression
1		nfal.1	⊢ Ⅎ 𝑥 𝜑
2	1	nf5ri	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
3	2	hbal	⊢ ( ∀ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜑 )
4	3	nf5i	⊢ Ⅎ 𝑥 ∀ 𝑦 𝜑