Theorem nfal 1933

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 1860	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1830	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1610	1 |- F/ x A. y ph

Syntax hints:   A.wal 1381   F/wnf 1603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-11 1828  ax-12 1840

This theorem depends on definitions:  df-bi 185  df-ex 1600  df-nf 1604

This theorem is referenced by:  nfnf  1935  nfald  1937  nfa2  1939  aaan  1961  pm11.53  1969  19.12vv  1972  cbv3  2001  cbval2  2013  nfsb4t  2116  euf  2278  mo2  2279  2eu3  2365  bm1.1  2426  bm1.1OLD  2427  nfnfc1  2608  nfnfc  2614  nfnfcALT  2615  nfeqOLD  2617  sbcnestgf  3825  dfnfc2  4252  nfdisj  4419  nfdisj1  4420  axrep1  4549  axrep2  4550  axrep3  4551  axrep4  4552  nffr  4843  zfcndrep  8995  zfcndinf  8999  mreexexd  14922  mptelee  24070  mo5f  27255  19.12b  29209  wl-sb8t  29975  wl-mo2t  29995  wl-mo3t  29996  wl-sb8eut  29997  mpt2bi123f  30546  pm11.57  31249  pm11.59  31251  bj-cbv3v  34030  bj-cbv2v  34037  bj-cbval2v  34044  bj-axrep1  34116  bj-axrep2  34117  bj-axrep3  34118  bj-axrep4  34119  ax11-pm2  34151  bj-nfnfc  34171