Theorem nfal 2008

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 1930	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1899	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1669	1 |- F/ x A. y ph

Syntax hints:   A.wal 1436   F/wnf 1662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-11 1897  ax-12 1910

This theorem depends on definitions:  df-bi 189  df-ex 1659  df-nf 1663

This theorem is referenced by:  nfnf  2010  nfald  2012  nfa2  2014  aaan  2035  pm11.53  2043  19.12vv  2046  cbv3  2074  cbval2  2086  nfsb4t  2188  euf  2278  mo2  2279  2eu3  2355  bm1.1  2407  nfnfc1  2588  nfnfc  2594  nfnfcALT  2595  nfeqOLD  2597  sbcnestgf  3820  dfnfc2  4243  nfdisj  4412  nfdisj1  4413  axrep1  4543  axrep2  4544  axrep3  4545  axrep4  4546  nffr  4833  zfcndrep  9052  zfcndinf  9056  mreexexd  15559  mptelee  24929  mo5f  28124  19.12b  30461  bj-cbv3v  31294  bj-cbv2v  31301  bj-cbval2v  31308  bj-axrep1  31379  bj-axrep2  31380  bj-axrep3  31381  bj-axrep4  31382  ax11-pm2  31414  bj-nfnfc  31438  wl-sb8t  31850  wl-mo2tf  31870  wl-eutf  31872  wl-mo2t  31874  wl-mo3t  31875  wl-sb8eut  31876  mpt2bi123f  32376  pm11.57  36715  pm11.59  36717