Theorem nfi 1391

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

Syntax hints:   -> wi 4   A.wal 1282   F/wnf 1389

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

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nfth  1393  nfnth  1394  nfe1  1425  nfdh  1457  nfv  1461  nfa1  1474  nfan1  1496  nfim1  1503  nfor  1506  nfal  1508  nfex  1568  nfae  1647  cbv3h  1671  nfs1  1730  nfs1v  1856  hbsb  1864  sbco2h  1879  hbsbd  1899  dvelimALT  1927  dvelimfv  1928  hbeu  1962  hbeud  1963  eu3h  1986  mo3h  1994  nfsab1  2071  nfsab  2073  nfcii  2210  nfcri  2213