Theorem nfal 1523

Description: If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfal.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfal	⊢ Ⅎ𝑥∀𝑦𝜑

Proof of Theorem nfal

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	nfri 1467	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 1421	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nfi 1406	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1297  Ⅎwnf 1404

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-4 1455

This theorem depends on definitions:  df-bi 116  df-nf 1405

This theorem is referenced by:  nfnf  1524  nfa2  1526  aaan  1534  cbv3  1688  cbv2  1693  nfald  1701  cbval2  1856  nfsb4t  1950  nfeuv  1978  mo23  2001  bm1.1  2085  nfnfc1  2243  nfnfc  2247  nfeq  2248  sbcnestgf  3001  dfnfc2  3701  nfdisjv  3864  nfdisj1  3865  nffr  4209  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  exmidunben  11731  bdsepnft  12666  bdsepnfALT  12668  setindft  12748  strcollnft  12767  strcollnfALT  12769