Theorem nfal 1556

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 1500	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1454	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1439	1 |- F/ x A. y ph

Syntax hints:   A.wal 1330   F/wnf 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-4 1488

This theorem depends on definitions:  df-bi 116  df-nf 1438

This theorem is referenced by:  nfnf  1557  nfa2  1559  aaan  1567  cbv3  1721  cbv2  1726  nfald  1734  cbval2  1894  nfsb4t  1990  nfeuv  2018  mo23  2041  bm1.1  2125  nfnfc1  2285  nfnfc  2289  nfeq  2290  sbcnestgf  3056  dfnfc2  3762  nfdisjv  3926  nfdisj1  3927  nffr  4279  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidunben  11975  bdsepnft  13256  bdsepnfALT  13258  setindft  13334  strcollnft  13353  pw1nct  13371