Theorem nfi 1473

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

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

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 1460

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

This theorem is referenced by:  nfth  1475  nfnth  1476  nfe1  1507  nfdh  1535  nfv  1539  nfa1  1552  nfan1  1575  nfim1  1582  nfor  1585  nfex  1648  nfae  1730  cbv3h  1754  nfs1  1820  nfs1v  1955  hbsb  1965  sbco2h  1980  hbsbd  1998  dvelimALT  2026  dvelimfv  2027  hbeu  2063  hbeud  2064  eu3h  2087  mo3h  2095  nfsab1  2183  nfsab  2185  nfcii  2327  nfcri  2330