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

Theorem 2p1e3 11189
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 11118 . 2 3 = (2 + 1)
21eqcomi 2660 1 (2 + 1) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  (class class class)co 6690  1c1 9975   + caddc 9977  2c2 11108  3c3 11109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-3 11118
This theorem is referenced by:  1p2e3  11190  cnm2m1cnm3  11323  6t5e30  11682  6t5e30OLD  11683  7t5e35  11689  8t4e32  11694  9t4e36  11703  decbin3  11722  halfthird  11723  fz0to3un2pr  12480  m1modge3gt1  12757  fac3  13107  hash3  13232  hashtplei  13304  hashtpg  13305  s3len  13685  repsw3  13740  bpoly3  14833  bpoly4  14834  nn0o1gt2  15144  flodddiv4  15184  3exp3  15845  13prm  15870  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem2  15892  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem4  15898  4001prm  15899  dcubic1lem  24615  dcubic2  24616  mcubic  24619  log2ublem3  24720  log2ub  24721  birthday  24726  chtub  24982  2lgsoddprmlem3c  25182  istrkg3ld  25405  usgr2wlkspthlem2  26710  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  umgrwwlks2on  26923  elwwlks2  26933  elwspths2spth  26934  clwwlknonex2lem1  27082  clwwlknonex2lem2  27083  3wlkdlem5  27141  3wlkdlem10  27147  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  frgrregord013  27382  ex-hash  27440  threehalves  29751  lmat22det  30016  fib3  30593  prodfzo03  30809  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  jm2.23  37880  lt3addmuld  39829  wallispilem4  40603  wallispi2lem1  40606  stirlinglem11  40619  fmtno0  41777  fmtno5lem4  41793  fmtno4prmfac  41809  fmtno4nprmfac193  41811  139prmALT  41836  31prm  41837  m7prm  41841  lighneallem4a  41850  41prothprmlem2  41860  sbgoldbalt  41994  bgoldbtbndlem1  42018  tgoldbachlt  42029  tgoldbachltOLD  42035  pgrpgt2nabl  42472
  Copyright terms: Public domain W3C validator