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  1951  hbsb  1961  sbco2h  1976  hbsbd  1994  dvelimALT  2022  dvelimfv  2023  hbeu  2059  hbeud  2060  eu3h  2083  mo3h  2091  nfsab1  2179  nfsab  2181  nfcii  2323  nfcri  2326