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

Syntax hints:   -. wn 3   F/wnf 1513

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-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-4 1563  ax-ial 1587

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

This theorem is referenced by:  nfdc  1711  19.32dc  1731  nfnae  1774  mo2n  2114  nfne  2513  nfnel  2522  nfdif  3350  rabsnifsb  3773  nfpo  4441  0neqopab  6123  nfsup  7322  ismkvnex  7485  mkvprop  7488  zsupcllemstep  10640  oddpwdclemndvds  12927  ismkvnnlem  17007