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  43261  wallispilem4  44031  wallispi2lem1  44034  stirlinglem11  44047  fmtno0  45450  fmtno5lem4  45466  fmtno4prmfac  45482  fmtno4nprmfac193  45484  139prmALT  45506  31prm  45507  m7prm  45510  lighneallem4a  45518  41prothprmlem2  45528  2exp340mod341  45643  sbgoldbalt  45691  bgoldbtbndlem1  45715  tgoldbachlt  45726  pgrpgt2nabl  46160  ackval2  46486  ackval3  46487  ackval0012  46493  ackval3012  46496
  Copyright terms: Public domain W3C validator