MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2p1e3 Structured version   Visualization version   GIF version

Theorem 2p1e3 11765
Description: 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
2p1e3 (2 + 1) = 3

Proof of Theorem 2p1e3
StepHypRef Expression
1 df-3 11687 . 2 3 = (2 + 1)
21eqcomi 2833 1 (2 + 1) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7138  1c1 10523   + caddc 10525  2c2 11678  3c3 11679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-3 11687
This theorem is referenced by:  1p2e3  11766  1p2e3ALT  11767  cnm2m1cnm3  11876  6t5e30  12191  7t5e35  12196  8t4e32  12201  9t4e36  12208  decbin3  12226  halfthird  12227  fz0to3un2pr  13002  fzo0to42pr  13117  m1modge3gt1  13279  fac3  13634  hash3  13761  hashtplei  13836  hashtpg  13837  s3len  14245  repsw3  14302  bpoly3  15401  bpoly4  15402  nn0o1gt2  15719  flodddiv4  15751  ge2nprmge4  16032  3exp3  16414  13prm  16438  37prm  16443  43prm  16444  83prm  16445  139prm  16446  163prm  16447  317prm  16448  631prm  16449  1259lem1  16453  1259lem2  16454  1259lem3  16455  1259lem4  16456  1259lem5  16457  1259prm  16458  2503lem2  16460  2503prm  16462  4001lem1  16463  4001lem2  16464  4001lem4  16466  4001prm  16467  mcubic  25422  log2ublem3  25523  log2ub  25524  birthday  25529  chtub  25785  2lgsoddprmlem3c  25985  istrkg3ld  26244  usgr2wlkspthlem2  27536  elwwlks2ons3im  27729  umgrwwlks2on  27732  elwwlks2  27741  elwspths2spth  27742  clwwlknonex2lem1  27881  clwwlknonex2lem2  27882  3wlkdlem5  27937  3wlkdlem10  27943  upgr3v3e3cycl  27954  upgr4cycl4dv4e  27959  konigsberglem1  28026  konigsberglem2  28027  konigsberglem3  28028  numclwlk1  28145  frgrregord013  28169  ex-hash  28227  threehalves  30588  lmat22det  31108  fib3  31679  prodfzo03  31892  hgt750lemd  31937  hgt750lem  31940  hgt750lem2  31941  3cubeslem3l  39459  3cubeslem3r  39460  jm2.23  39769  resqrtvalex  40177  lt3addmuld  41775  wallispilem4  42552  wallispi2lem1  42555  stirlinglem11  42568  fmtno0  43899  fmtno5lem4  43915  fmtno4prmfac  43931  fmtno4nprmfac193  43933  139prmALT  43955  31prm  43956  m7prm  43959  lighneallem4a  43968  41prothprmlem2  43978  2exp340mod341  44093  sbgoldbalt  44141  bgoldbtbndlem1  44165  tgoldbachlt  44176  pgrpgt2nabl  44609  ackval2  44926  ackval3  44927  ackval0012  44933  ackval3012  44936
  Copyright terms: Public domain W3C validator