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

Theorem 2p1e3 12228
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 12150 . 2 3 = (2 + 1)
21eqcomi 2746 1 (2 + 1) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7349  1c1 10985   + caddc 10987  2c2 12141  3c3 12142
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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2729  df-3 12150
This theorem is referenced by:  1p2e3  12229  1p2e3ALT  12230  cnm2m1cnm3  12339  6t5e30  12657  7t5e35  12662  8t4e32  12667  9t4e36  12674  decbin3  12692  halfthird  12693  fz0to3un2pr  13471  fzo0to42pr  13587  m1modge3gt1  13751  fac3  14107  hash3  14233  hashtplei  14310  hashtpg  14311  s3len  14714  repsw3  14771  bpoly3  15875  bpoly4  15876  nn0o1gt2  16197  flodddiv4  16229  ge2nprmge4  16511  3exp3  16898  13prm  16922  37prm  16927  43prm  16928  83prm  16929  139prm  16930  163prm  16931  317prm  16932  631prm  16933  1259lem1  16937  1259lem2  16938  1259lem3  16939  1259lem4  16940  1259lem5  16941  1259prm  16942  2503lem2  16944  2503prm  16946  4001lem1  16947  4001lem2  16948  4001lem4  16950  4001prm  16951  mcubic  26119  log2ublem3  26220  log2ub  26221  birthday  26226  chtub  26482  2lgsoddprmlem3c  26682  istrkg3ld  27201  usgr2wlkspthlem2  28504  elwwlks2ons3im  28697  umgrwwlks2on  28700  elwwlks2  28709  elwspths2spth  28710  clwwlknonex2lem1  28849  clwwlknonex2lem2  28850  3wlkdlem5  28905  3wlkdlem10  28911  upgr3v3e3cycl  28922  upgr4cycl4dv4e  28927  konigsberglem1  28994  konigsberglem2  28995  konigsberglem3  28996  numclwlk1  29113  frgrregord013  29137  ex-hash  29195  threehalves  31565  lmat22det  32176  fib3  32776  prodfzo03  32989  hgt750lemd  33034  hgt750lem  33037  hgt750lem2  33038  aks4d1p1p2  40422  aks4d1p1p7  40426  aks4d1p1  40428  2np3bcnp1  40447  3cubeslem3l  40874  3cubeslem3r  40875  jm2.23  41185  resqrtvalex  41679  lt3addmuld  43292  wallispilem4  44062  wallispi2lem1  44065  stirlinglem11  44078  fmtno0  45481  fmtno5lem4  45497  fmtno4prmfac  45513  fmtno4nprmfac193  45515  139prmALT  45537  31prm  45538  m7prm  45541  lighneallem4a  45549  41prothprmlem2  45559  2exp340mod341  45674  sbgoldbalt  45722  bgoldbtbndlem1  45746  tgoldbachlt  45757  pgrpgt2nabl  46191  ackval2  46517  ackval3  46518  ackval0012  46524  ackval3012  46527
  Copyright terms: Public domain W3C validator