Theorem nfn 1710

Description: Inference associated with nfnt 1708. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfn.1	|- F/ x ph

Assertion

Ref	Expression
nfn	|- F/ x -. ph

Proof of Theorem nfn

Step	Hyp	Ref	Expression
1		nfn.1	. 2 |- F/ x ph
2		nfnt 1708	. 2 |- ( F/ x ph -> F/ x -. ph )
3	1, 2	ax-mp 5	1 |- F/ x -. ph

This proof depends on syntax axioms:   -. wn 3   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408  df-nf 1514

This theorem is used by:  nfdc  1711  19.32dc  1731  nfnae  1774  mo2n  2114  nfne  2513  nfnel  2522  nfdif  3350  rabsnifsb  3777  nfpo  4446  0neqopab  6133  nfsup  7332  ismkvnex  7495  mkvprop  7498  zsupcllemstep  10662  oddpwdclemndvds  12949  ismkvnnlem  17102