Theorem nfi 1486

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

Syntax hints:   -> wi 4   A.wal 1371   F/wnf 1484

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 1473

This theorem depends on definitions:  df-bi 117  df-nf 1485

This theorem is referenced by:  nfth  1488  nfnth  1489  nfe1  1520  nfdh  1548  nfv  1552  nfa1  1565  nfan1  1588  nfim1  1595  nfor  1598  nfex  1661  nfae  1743  cbv3h  1767  nfs1  1833  nfs1v  1968  hbsb  1978  sbco2h  1993  hbsbd  2011  dvelimALT  2039  dvelimfv  2040  hbeu  2076  hbeud  2077  eu3h  2100  mo3h  2108  nfsab1  2196  nfsab  2198  nfcii  2340  nfcri  2343