Theorem nfi 1508

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 1507	. 2 |- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
2		nfi.1	. 2 |- ( ph -> A. x ph )
3	1, 2	mpgbir 1499	1 |- F/ x ph

Syntax hints:   -> wi 4   A.wal 1393   F/wnf 1506

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 1495

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

This theorem is referenced by:  nfth  1510  nfnth  1511  nfe1  1542  nfdh  1570  nfv  1574  nfa1  1587  nfan1  1610  nfim1  1617  nfor  1620  nfex  1683  nfae  1765  cbv3h  1789  nfs1  1855  nfs1v  1990  hbsb  2000  sbco2h  2015  hbsbd  2033  dvelimALT  2061  dvelimfv  2062  hbeu  2098  hbeud  2099  eu3h  2123  mo3h  2131  nfsab1  2219  nfsab  2221  nfcii  2363  nfcri  2366