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

Theorem 2p1e3 10655
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 10591 . 2  |-  3  =  ( 2  +  1 )
21eqcomi 2480 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379  (class class class)co 6282   1c1 9489    + caddc 9491   2c2 10581   3c3 10582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-3 10591
This theorem is referenced by:  1p2e3  10656  cnm2m1cnm3  10786  6t5e30  11052  7t5e35  11057  8t4e32  11062  9t4e36  11069  decbin3  11077  f13idfv  12070  fac3  12324  hash3  12433  hashtplei  12484  hashtpg  12485  s3len  12815  repsw3  12848  prmn2uzge3  14092  3exp3  14430  13prm  14455  37prm  14460  43prm  14461  83prm  14462  139prm  14463  163prm  14464  317prm  14465  631prm  14466  1259lem1  14467  1259lem2  14468  1259lem4  14470  1259lem5  14471  1259prm  14472  2503lem2  14474  2503prm  14476  4001lem1  14477  4001lem2  14478  4001lem4  14480  4001prm  14481  dcubic1lem  22902  dcubic2  22903  mcubic  22906  log2ublem3  23007  log2ub  23008  birthday  23012  chtub  23215  3v3e3cycl1  24320  constr3trllem5  24330  4cycl4v4e  24342  4cycl4dv4e  24344  extwwlkfablem2  24755  numclwwlkovf2ex  24763  frgraregord013  24795  fib3  27982  halfthird  28588  bpoly3  29397  bpoly4  29398  jm2.23  30542  lt3addmuld  31078  wallispilem4  31368  wallispi2lem1  31371  stirlinglem11  31384  pgrpgt2nabl  32024
  Copyright terms: Public domain W3C validator