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

Theorem 2p1e3 10723
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 10658 . 2  |-  3  =  ( 2  +  1 )
21eqcomi 2461 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff setvar class
Syntax hints:    = wceq 1448  (class class class)co 6276   1c1 9527    + caddc 9529   2c2 10648   3c3 10649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-cleq 2445  df-3 10658
This theorem is referenced by:  1p2e3  10724  cnm2m1cnm3  10854  6t5e30  11121  7t5e35  11126  8t4e32  11131  9t4e36  11138  decbin3  11146  halfthird  11147  fz0to3un2pr  11885  fac3  12460  hash3  12577  hashtplei  12635  hashtpg  12636  s3len  12987  repsw3  13037  bpoly3  14122  bpoly4  14123  prmn2uzge3  14655  3exp3  15073  13prm  15098  37prm  15103  43prm  15104  83prm  15105  139prm  15106  163prm  15107  317prm  15108  631prm  15109  1259lem1  15113  1259lem2  15114  1259lem4  15116  1259lem5  15117  1259prm  15118  2503lem2  15120  2503prm  15122  4001lem1  15123  4001lem2  15124  4001lem4  15126  4001prm  15127  dcubic1lem  23781  dcubic2  23782  mcubic  23785  log2ublem3  23886  log2ub  23887  birthday  23892  chtub  24152  istrkg3ld  24521  3v3e3cycl1  25384  constr3trllem5  25394  4cycl4v4e  25406  4cycl4dv4e  25408  extwwlkfablem2  25818  numclwwlkovf2ex  25826  frgraregord013  25858  lmat22det  28655  fib3  29242  jm2.23  35853  lt3addmuld  37550  wallispilem4  37987  wallispi2lem1  37990  stirlinglem11  38003  sgoldbalt  38973  bgoldbtbndlem1  38991  tgoldbachlt  39000  41prothprmlem2  39009  usgr2wlkspthlem2  39842  31wlkdlem5  39956  31wlkdlem10  39962  upgr3v3e3cycl  39973  upgr4cycl4dv4e  39978  pgrpgt2nabl  40476  nn0o1gt2  40652
  Copyright terms: Public domain W3C validator