Theorem nfal 2005

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 1927	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1896	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1670	1 |- F/ x A. y ph

Syntax hints:   A.wal 1435   F/wnf 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-11 1894  ax-12 1907

This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664

This theorem is referenced by:  nfnf  2007  nfald  2009  nfa2  2011  aaan  2032  pm11.53  2040  19.12vv  2043  cbv3  2071  cbval2  2083  nfsb4t  2184  euf  2276  mo2  2277  2eu3  2357  bm1.1  2412  bm1.1OLD  2413  nfnfc1  2594  nfnfc  2600  nfnfcALT  2601  nfeqOLD  2603  sbcnestgf  3818  dfnfc2  4240  nfdisj  4409  nfdisj1  4410  axrep1  4539  axrep2  4540  axrep3  4541  axrep4  4542  nffr  4828  zfcndrep  9038  zfcndinf  9042  mreexexd  15505  mptelee  24771  mo5f  27955  19.12b  30235  bj-cbv3v  31068  bj-cbv2v  31075  bj-cbval2v  31082  bj-axrep1  31154  bj-axrep2  31155  bj-axrep3  31156  bj-axrep4  31157  ax11-pm2  31189  bj-nfnfc  31213  wl-sb8t  31587  wl-mo2tf  31607  wl-mo2t  31608  wl-mo3t  31609  wl-sb8eut  31610  mpt2bi123f  32110  pm11.57  36376  pm11.59  36378