Theorem nfi 1438

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

Syntax hints:   -> wi 4   A.wal 1329   F/wnf 1436

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

This theorem depends on definitions:  df-bi 116  df-nf 1437

This theorem is referenced by:  nfth  1440  nfnth  1441  nfe1  1472  nfdh  1504  nfv  1508  nfa1  1521  nfan1  1543  nfim1  1550  nfor  1553  nfal  1555  nfex  1616  nfae  1697  cbv3h  1721  nfs1  1781  nfs1v  1910  hbsb  1920  sbco2h  1935  hbsbd  1955  dvelimALT  1983  dvelimfv  1984  hbeu  2018  hbeud  2019  eu3h  2042  mo3h  2050  nfsab1  2127  nfsab  2129  nfcii  2270  nfcri  2273