Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfn Structured version   Unicode version

Theorem nfn 1956
 Description: Inference associated with nfnt 1955. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfn.1
Assertion
Ref Expression
nfn

Proof of Theorem nfn
StepHypRef Expression
1 nfn.1 . 2
2 nfnt 1955 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wn 3  wnf 1663 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-12 1905 This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664 This theorem is referenced by:  nfna1  1958  nfnan  1985  nfor  1991  19.32  2022  cbvex  2076  cbvex2  2082  nfnae  2113  axc14  2166  euor  2308  euor2  2310  nfne  2756  nfnel  2768  nfrexOLD  2889  cbvrexf  3050  spcimegf  3160  spcegf  3162  cbvrexcsf  3428  nfdif  3586  rabsnifsb  4065  nfpo  4775  nffr  4823  rexxpf  4997  0neqopab  6345  boxcutc  7569  nfoi  8031  rabssnn0fi  12197  fsuppmapnn0fiubex  12203  spc2d  28090  ordtconlem1  28723  esumrnmpt2  28882  ddemeas  29052  bnj1476  29651  bnj1388  29835  bnj1398  29836  bnj1445  29846  bnj1449  29850  bj-cbvexv  31282  bj-cbvex2v  31288  wl-nfnae1  31772  cdlemefs32sn1aw  33897  ss2iundf  36108  ax6e2ndeqALT  37186  uzwo4  37251  stoweidlem34  37712  stoweidlem55  37733  stoweidlem59  37737  etransclem32  37948  sge0f1o  38009  r19.32  38298
 Copyright terms: Public domain W3C validator