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

Theorem 2p1e3 11096
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 11025 . 2 3 = (2 + 1)
21eqcomi 2635 1 (2 + 1) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6605  1c1 9882   + caddc 9884  2c2 11015  3c3 11016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2619  df-3 11025
This theorem is referenced by:  1p2e3  11097  cnm2m1cnm3  11230  6t5e30  11588  6t5e30OLD  11589  7t5e35  11595  8t4e32  11600  9t4e36  11609  decbin3  11628  halfthird  11629  fz0to3un2pr  12379  m1modge3gt1  12654  fac3  13004  hash3  13131  hashtplei  13199  hashtpg  13200  s3len  13570  repsw3  13623  bpoly3  14709  bpoly4  14710  nn0o1gt2  15016  flodddiv4  15056  3exp3  15717  13prm  15742  37prm  15747  43prm  15748  83prm  15749  139prm  15750  163prm  15751  317prm  15752  631prm  15753  1259lem1  15757  1259lem2  15758  1259lem3  15759  1259lem4  15760  1259lem5  15761  1259prm  15762  2503lem2  15764  2503prm  15766  4001lem1  15767  4001lem2  15768  4001lem4  15770  4001prm  15771  dcubic1lem  24465  dcubic2  24466  mcubic  24469  log2ublem3  24570  log2ub  24571  birthday  24576  chtub  24832  2lgsoddprmlem3c  25032  istrkg3ld  25255  usgr2wlkspthlem2  26517  wwlks2onv  26710  elwwlks2ons3  26711  umgrwwlks2on  26713  elwwlks2  26722  elwspths2spth  26723  3wlkdlem5  26883  3wlkdlem10  26889  upgr3v3e3cycl  26900  upgr4cycl4dv4e  26905  konigsberglem1  26974  konigsberglem2  26975  konigsberglem3  26976  numclwwlkovf2ex  27069  frgrregord013  27101  ex-hash  27158  lmat22det  29662  fib3  30238  jm2.23  37029  lt3addmuld  38966  wallispilem4  39579  wallispi2lem1  39582  stirlinglem11  39595  fmtno0  40739  fmtno5lem4  40755  fmtno4prmfac  40771  fmtno4nprmfac193  40773  139prmALT  40798  31prm  40799  m7prm  40803  lighneallem4a  40812  41prothprmlem2  40822  sgoldbalt  40952  bgoldbtbndlem1  40970  tgoldbachlt  40979  tgoldbachltOLD  40986  pgrpgt2nabl  41409
  Copyright terms: Public domain W3C validator