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

Theorem 2p1e3 10684
Description: 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
2p1e3

Proof of Theorem 2p1e3
StepHypRef Expression
1 df-3 10620 . 2
21eqcomi 2470 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296  1c1 9514   caddc 9516  2c2 10610  3c3 10611
This theorem is referenced by:  1p2e3  10685  cnm2m1cnm3  10815  6t5e30  11084  7t5e35  11089  8t4e32  11094  9t4e36  11101  decbin3  11109  fac3  12360  hash3  12471  hashtplei  12522  hashtpg  12523  s3len  12856  repsw3  12889  prmn2uzge3  14237  3exp3  14576  13prm  14601  37prm  14606  43prm  14607  83prm  14608  139prm  14609  163prm  14610  317prm  14611  631prm  14612  1259lem1  14613  1259lem2  14614  1259lem4  14616  1259lem5  14617  1259prm  14618  2503lem2  14620  2503prm  14622  4001lem1  14623  4001lem2  14624  4001lem4  14626  4001prm  14627  dcubic1lem  23174  dcubic2  23175  mcubic  23178  log2ublem3  23279  log2ub  23280  birthday  23284  chtub  23487  3v3e3cycl1  24644  constr3trllem5  24654  4cycl4v4e  24666  4cycl4dv4e  24668  extwwlkfablem2  25078  numclwwlkovf2ex  25086  frgraregord013  25118  fib3  28342  halfthird  29113  bpoly3  29820  bpoly4  29821  jm2.23  30938  lt3addmuld  31501  wallispilem4  31850  wallispi2lem1  31853  stirlinglem11  31866  pgrpgt2nabl  32959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-3 10620
  Copyright terms: Public domain W3C validator