Theorem nfal 1468

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 1412	. . 3 |- ( ph -> A. x ph )
3	2	hbal 1366	. 2 |- ( A. y ph -> A. x A. y ph )
4	3	nfi 1351	1 |- F/ x A. y ph

Syntax hints:   A.wal 1241   F/wnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-4 1400

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  nfnf  1469  nfa2  1471  aaan  1479  cbv3  1630  cbv2  1635  nfald  1643  cbval2  1796  nfsb4t  1890  nfeuv  1918  mo23  1941  bm1.1  2025  nfnfc1  2181  nfnfc  2184  nfeq  2185  sbcnestgf  2897  dfnfc2  3598  nfdisjv  3757  nfdisj1  3758  nffr  4086  bdsepnft  10007  bdsepnfALT  10009  setindft  10090  strcollnft  10109  strcollnfALT  10111