Theorem nfal 1508

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 1452	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1406	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1391	1 |- F/ x A. y ph

Syntax hints:   A.wal 1282   F/wnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-4 1440

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nfnf  1509  nfa2  1511  aaan  1519  cbv3  1670  cbv2  1675  nfald  1683  cbval2  1837  nfsb4t  1931  nfeuv  1959  mo23  1982  bm1.1  2066  nfnfc1  2222  nfnfc  2225  nfeq  2226  sbcnestgf  2953  dfnfc2  3619  nfdisjv  3778  nfdisj1  3779  nffr  4104  bdsepnft  10678  bdsepnfALT  10680  setindft  10760  strcollnft  10779  strcollnfALT  10781