Theorem nfi 1439

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

Syntax hints:   -> wi 4   A.wal 1330   F/wnf 1437

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 1426

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

This theorem is referenced by:  nfth  1441  nfnth  1442  nfe1  1473  nfdh  1505  nfv  1509  nfa1  1522  nfan1  1544  nfim1  1551  nfor  1554  nfal  1556  nfex  1617  nfae  1698  cbv3h  1722  nfs1  1782  nfs1v  1913  hbsb  1923  sbco2h  1938  hbsbd  1958  dvelimALT  1986  dvelimfv  1987  hbeu  2021  hbeud  2022  eu3h  2045  mo3h  2053  nfsab1  2130  nfsab  2132  nfcii  2273  nfcri  2276