Theorem nfn 1901

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

Hypothesis

Ref	Expression
nfn.1

Assertion

Ref	Expression
nfn

Proof of Theorem nfn

Step	Hyp	Ref	Expression
1		nfn.1	. 2
2		nfnt 1900	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  -.wn 3  F/wnf 1616

This theorem is referenced by:  nfna1  1903  nfnan  1929  nfor  1935  19.32  1967  cbvex  2022  cbvex2  2028  nfnae  2058  axc14  2113  euor  2331  euor2  2333  nfne  2788  nfnel  2800  nfrexOLD  2921  cbvrexf  3079  spcimegf  3188  spcegf  3190  cbvrexcsf  3467  nfdif  3624  rabsnifsb  4098  nfpo  4810  nffr  4858  rexxpf  5155  0neqopab  6341  boxcutc  7532  nfoi  7960  rabssnn0fi  12095  fsuppmapnn0fiubex  12098  spc2d  27373  ordtconlem1  27906  ddemeas  28208  wl-nfnae1  29981  stoweidlem34  31816  stoweidlem55  31837  stoweidlem59  31841  etransclem32  32049  r19.32  32172  ax6e2ndeqALT  33731  bnj1476  33905  bnj1388  34089  bnj1398  34090  bnj1445  34100  bnj1449  34104  bj-cbvexv  34297  bj-cbvex2v  34303  cdlemefs32sn1aw  36140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617