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

Theorem 2p1e3 12229
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 12151 . 2 3 = (2 + 1)
21eqcomi 2747 1 (2 + 1) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7350  1c1 10986   + caddc 10988  2c2 12142  3c3 12143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2730  df-3 12151
This theorem is referenced by:  1p2e3  12230  1p2e3ALT  12231  cnm2m1cnm3  12340  6t5e30  12658  7t5e35  12663  8t4e32  12668  9t4e36  12675  decbin3  12693  halfthird  12694  fz0to3un2pr  13472  fzo0to42pr  13588  m1modge3gt1  13752  fac3  14108  hash3  14234  hashtplei  14311  hashtpg  14312  s3len  14715  repsw3  14772  bpoly3  15876  bpoly4  15877  nn0o1gt2  16198  flodddiv4  16230  ge2nprmge4  16512  3exp3  16899  13prm  16923  37prm  16928  43prm  16929  83prm  16930  139prm  16931  163prm  16932  317prm  16933  631prm  16934  1259lem1  16938  1259lem2  16939  1259lem3  16940  1259lem4  16941  1259lem5  16942  1259prm  16943  2503lem2  16945  2503prm  16947  4001lem1  16948  4001lem2  16949  4001lem4  16951  4001prm  16952  mcubic  26119  log2ublem3  26220  log2ub  26221  birthday  26226  chtub  26482  2lgsoddprmlem3c  26682  istrkg3ld  27189  usgr2wlkspthlem2  28492  elwwlks2ons3im  28685  umgrwwlks2on  28688  elwwlks2  28697  elwspths2spth  28698  clwwlknonex2lem1  28837  clwwlknonex2lem2  28838  3wlkdlem5  28893  3wlkdlem10  28899  upgr3v3e3cycl  28910  upgr4cycl4dv4e  28915  konigsberglem1  28982  konigsberglem2  28983  konigsberglem3  28984  numclwlk1  29101  frgrregord013  29125  ex-hash  29183  threehalves  31553  lmat22det  32164  fib3  32764  prodfzo03  32977  hgt750lemd  33022  hgt750lem  33025  hgt750lem2  33026  aks4d1p1p2  40413  aks4d1p1p7  40417  aks4d1p1  40419  2np3bcnp1  40438  3cubeslem3l  40843  3cubeslem3r  40844  jm2.23  41154  resqrtvalex  41648  lt3addmuld  43249  wallispilem4  44019  wallispi2lem1  44022  stirlinglem11  44035  fmtno0  45432  fmtno5lem4  45448  fmtno4prmfac  45464  fmtno4nprmfac193  45466  139prmALT  45488  31prm  45489  m7prm  45492  lighneallem4a  45500  41prothprmlem2  45510  2exp340mod341  45625  sbgoldbalt  45673  bgoldbtbndlem1  45697  tgoldbachlt  45708  pgrpgt2nabl  46142  ackval2  46468  ackval3  46469  ackval0012  46475  ackval3012  46478
  Copyright terms: Public domain W3C validator