Theorem nfal 1894

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

Hypothesis

Ref	Expression
nfal.1	|- F/ x ph

Assertion

Ref	Expression
nfal	|- F/ x A. y ph

Proof of Theorem nfal

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4 |- F/ x ph
2	1	nfri 1822	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1793	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1606	1 |- F/ x A. y ph

Syntax hints:   A.wal 1377   F/wnf 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-11 1791  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600

This theorem is referenced by:  nfnf  1896  nfald  1898  nfa2  1900  aaan  1924  pm11.53  1937  19.12vv  1942  cbv3  1984  cbv2  1992  cbval2  2000  nfsb4t  2103  euf  2285  eufOLD  2286  mo2  2287  moOLD  2327  2moOLDOLD  2384  2eu3  2389  bm1.1  2450  bm1.1OLD  2451  nfnfc1  2632  nfnfc  2638  nfnfcALT  2639  nfeqOLD  2641  sbcnestgf  3839  dfnfc2  4263  nfdisj  4429  nfdisj1  4430  axrep1  4559  axrep2  4560  axrep3  4561  axrep4  4562  nffr  4853  zfcndrep  8991  zfcndinf  8995  mreexexd  14902  mptelee  23890  mo5f  27075  19.12b  28827  wl-sb8t  29593  wl-mo2t  29613  wl-mo3t  29614  wl-sb8eut  29615  mpt2bi123f  30191  pm11.57  30889  pm11.59  30891  bj-cbv3v  33379  bj-cbv2v  33386  bj-cbval2v  33393  bj-axrep1  33464  bj-axrep2  33465  bj-axrep3  33466  bj-axrep4  33467  ax11-pm2  33499  bj-nfnfc  33519