Theorem nfal 1873

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 1808	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1782	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1596	1 |- F/ x A. y ph

Syntax hints:   A.wal 1367   F/wnf 1589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-11 1780  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590

This theorem is referenced by:  nfnf  1875  nfald  1877  nfa2  1879  aaan  1903  pm11.53  1912  19.12vv  1917  cbv3  1959  cbv2  1967  cbval2  1975  nfsb4t  2080  euf  2263  eufOLD  2264  mo2  2265  moOLD  2305  2moOLDOLD  2362  2eu3  2367  bm1.1  2427  bm1.1OLD  2428  nfnfc1  2582  nfnfc  2585  nfeq  2586  sbcnestgf  3691  dfnfc2  4109  nfdisj  4274  nfdisj1  4275  axrep1  4404  axrep2  4405  axrep3  4406  axrep4  4407  nffr  4694  zfcndrep  8781  zfcndinf  8785  mreexexd  14586  mptelee  23141  mo5f  25868  19.12b  27615  wl-sb8t  28376  wl-mo2t  28396  wl-mo3t  28397  wl-sb8eut  28398  mpt2bi123f  28975  pm11.57  29642  pm11.59  29644  bj-cbv3v  32224  bj-cbv2v  32231  bj-cbval2v  32238  bj-axrep1  32309  bj-axrep2  32310  bj-axrep3  32311  bj-axrep4  32312  ax11-pm2  32344  bj-nfnfc  32364