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  1501  nfv  1505  nfa1  1518  nfan1  1541  nfim1  1548  nfor  1551  nfex  1614  nfae  1696  cbv3h  1720  nfs1  1786  nfs1v  1916  hbsb  1926  sbco2h  1941  hbsbd  1959  dvelimALT  1987  dvelimfv  1988  hbeu  2024  hbeud  2025  eu3h  2048  mo3h  2056  nfsab1  2144  nfsab  2146  nfcii  2287  nfcri  2290