Theorem nfi 1511

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

Syntax hints:   -> wi 4   A.wal 1396   F/wnf 1509

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 1498

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

This theorem is referenced by:  nfth  1513  nfnth  1514  nfe1  1545  nfdh  1573  nfv  1577  nfa1  1590  nfan1  1613  nfim1  1620  nfor  1623  nfex  1686  nfae  1767  cbv3h  1792  nfs1  1858  nfs1v  1995  hbsb  2005  sbco2h  2020  hbsbd  2038  dvelimALT  2066  dvelimfv  2067  hbeu  2103  hbeud  2104  eu3h  2128  mo3h  2136  nfsab1  2224  nfsab  2226  nfcii  2377  nfcri  2380