Theorem nfal 1509

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 1453	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1407	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1392	1 |- F/ x A. y ph

Syntax hints:   A.wal 1283   F/wnf 1390

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 1377  ax-7 1378  ax-gen 1379  ax-4 1441

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

This theorem is referenced by:  nfnf  1510  nfa2  1512  aaan  1520  cbv3  1671  cbv2  1676  nfald  1684  cbval2  1838  nfsb4t  1932  nfeuv  1960  mo23  1983  bm1.1  2067  nfnfc1  2223  nfnfc  2226  nfeq  2227  sbcnestgf  2954  dfnfc2  3627  nfdisjv  3786  nfdisj1  3787  nffr  4112  bdsepnft  10836  bdsepnfALT  10838  setindft  10918  strcollnft  10937  strcollnfALT  10939