Theorem nfal 1952

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 1879	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1849	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1628	1 |- F/ x A. y ph

Syntax hints:   A.wal 1396   F/wnf 1621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-11 1847  ax-12 1859

This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622

This theorem is referenced by:  nfnf  1954  nfald  1956  nfa2  1958  aaan  1980  pm11.53  1988  19.12vv  1991  cbv3  2020  cbval2  2032  nfsb4t  2132  euf  2294  mo2  2295  2eu3  2376  bm1.1  2437  bm1.1OLD  2438  nfnfc1  2619  nfnfc  2625  nfnfcALT  2626  nfeqOLD  2628  sbcnestgf  3834  dfnfc2  4253  nfdisj  4422  nfdisj1  4423  axrep1  4551  axrep2  4552  axrep3  4553  axrep4  4554  nffr  4842  zfcndrep  8981  zfcndinf  8985  mreexexd  15137  mptelee  24400  mo5f  27581  19.12b  29474  wl-sb8t  30240  wl-mo2t  30260  wl-mo3t  30261  wl-sb8eut  30262  mpt2bi123f  30811  pm11.57  31536  pm11.59  31538  bj-cbv3v  34689  bj-cbv2v  34696  bj-cbval2v  34703  bj-axrep1  34775  bj-axrep2  34776  bj-axrep3  34777  bj-axrep4  34778  ax11-pm2  34810  bj-nfnfc  34830