Theorem nfal 2316

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	nf5ri 2218	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 2191	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nf5i 2178	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1628  Ⅎwnf 1855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-10 2173  ax-11 2189  ax-12 2202

This theorem depends on definitions:  df-bi 197  df-ex 1852  df-nf 1857

This theorem is referenced by:  nfex  2317  nfnf  2321  nfaldOLD  2327  nfa2OLD  2329  aaan  2330  cbv3v  2332  pm11.53  2340  19.12vv  2341  cbv3  2425  cbval2  2437  nfsb4t  2535  euf  2625  mo2  2626  2eu3  2703  bm1.1  2755  nfnfc1  2915  nfnfc  2922  nfnfcALT  2923  sbcnestgf  4137  nfdisj  4764  nfdisj1  4765  axrep1  4903  axrep2  4904  axrep3  4905  axrep4  4906  nffr  5223  zfcndrep  9637  zfcndinf  9641  mreexexd  16515  mptelee  25995  mo5f  29658  19.12b  32037  bj-cbv2v  33062  bj-cbval2v  33067  bj-axrep1  33118  bj-axrep2  33119  bj-axrep3  33120  bj-axrep4  33121  ax11-pm2  33152  wl-sb8t  33661  wl-mo2tf  33680  wl-eutf  33682  wl-mo2t  33684  wl-mo3t  33685  wl-sb8eut  33686  mpt2bi123f  34296  pm11.57  39108  pm11.59  39110  nfsetrecs  42951