Theorem nfi 1462

Description: Deduce that x is not free in ph from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfi.1	|- ( ph -> A. x ph )

Assertion

Ref	Expression
nfi	|- F/ x ph

Proof of Theorem nfi

Step	Hyp	Ref	Expression
1		df-nf 1461	. 2 |- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
2		nfi.1	. 2 |- ( ph -> A. x ph )
3	1, 2	mpgbir 1453	1 |- F/ x ph

Syntax hints:   -> wi 4   A.wal 1351   F/wnf 1460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449

This theorem depends on definitions:  df-bi 117  df-nf 1461

This theorem is referenced by:  nfth  1464  nfnth  1465  nfe1  1496  nfdh  1524  nfv  1528  nfa1  1541  nfan1  1564  nfim1  1571  nfor  1574  nfex  1637  nfae  1719  cbv3h  1743  nfs1  1809  nfs1v  1939  hbsb  1949  sbco2h  1964  hbsbd  1982  dvelimALT  2010  dvelimfv  2011  hbeu  2047  hbeud  2048  eu3h  2071  mo3h  2079  nfsab1  2167  nfsab  2169  nfcii  2310  nfcri  2313