Theorem nfi 1476

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

Syntax hints:   -> wi 4   A.wal 1362   F/wnf 1474

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 1463

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

This theorem is referenced by:  nfth  1478  nfnth  1479  nfe1  1510  nfdh  1538  nfv  1542  nfa1  1555  nfan1  1578  nfim1  1585  nfor  1588  nfex  1651  nfae  1733  cbv3h  1757  nfs1  1823  nfs1v  1958  hbsb  1968  sbco2h  1983  hbsbd  2001  dvelimALT  2029  dvelimfv  2030  hbeu  2066  hbeud  2067  eu3h  2090  mo3h  2098  nfsab1  2186  nfsab  2188  nfcii  2330  nfcri  2333