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 2467 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398  (class class class)co 6270   1c1 9482    + caddc 9484   2c2 10581   3c3 10582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-3 10591
This theorem is referenced by:  1p2e3  10656  cnm2m1cnm3  10786  6t5e30  11056  7t5e35  11061  8t4e32  11066  9t4e36  11073  decbin3  11081  fac3  12342  hash3  12455  hashtplei  12506  hashtpg  12507  s3len  12847  repsw3  12880  prmn2uzge3  14321  3exp3  14660  13prm  14685  37prm  14690  43prm  14691  83prm  14692  139prm  14693  163prm  14694  317prm  14695  631prm  14696  1259lem1  14697  1259lem2  14698  1259lem4  14700  1259lem5  14701  1259prm  14702  2503lem2  14704  2503prm  14706  4001lem1  14707  4001lem2  14708  4001lem4  14710  4001prm  14711  dcubic1lem  23371  dcubic2  23372  mcubic  23375  log2ublem3  23476  log2ub  23477  birthday  23482  chtub  23685  3v3e3cycl1  24846  constr3trllem5  24856  4cycl4v4e  24868  4cycl4dv4e  24870  extwwlkfablem2  25280  numclwwlkovf2ex  25288  frgraregord013  25320  fib3  28606  halfthird  29354  bpoly3  30048  bpoly4  30049  jm2.23  31177  lt3addmuld  31740  wallispilem4  32089  wallispi2lem1  32092  stirlinglem11  32105  pgrpgt2nabl  33213  nn0o1gt2  33391
  Copyright terms: Public domain W3C validator