Theorem nfal 2049

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 1972	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1939	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1682	1 |- F/ x A. y ph

Syntax hints:   A.wal 1450   F/wnf 1675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-11 1937  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676

This theorem is referenced by:  nfnf  2051  nfald  2053  nfa2  2055  aaan  2074  cbv3v  2078  pm11.53  2090  19.12vv  2091  cbv3  2121  cbval2  2133  nfsb4t  2238  euf  2327  mo2  2328  2eu3  2404  bm1.1  2456  nfnfc1  2615  nfnfc  2621  nfnfcALT  2622  sbcnestgf  3788  dfnfc2  4208  nfdisj  4378  nfdisj1  4379  axrep1  4509  axrep2  4510  axrep3  4511  axrep4  4512  nffr  4813  zfcndrep  9057  zfcndinf  9061  mreexexd  15632  mptelee  25004  mo5f  28199  19.12b  30519  bj-cbv2v  31399  bj-cbval2v  31404  bj-axrep1  31469  bj-axrep2  31470  bj-axrep3  31471  bj-axrep4  31472  ax11-pm2  31504  bj-nfnfc  31530  wl-sb8t  31950  wl-mo2tf  31970  wl-eutf  31972  wl-mo2t  31974  wl-mo3t  31975  wl-sb8eut  31976  mpt2bi123f  32470  pm11.57  36809  pm11.59  36811