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

Theorem 2p1e3 10532
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 10468 . 2  |-  3  =  ( 2  +  1 )
21eqcomi 2462 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370  (class class class)co 6176   1c1 9370    + caddc 9372   2c2 10458   3c3 10459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-12 1793  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-cleq 2442  df-3 10468
This theorem is referenced by:  1p2e3  10533  6t5e30  10922  7t5e35  10927  8t4e32  10932  9t4e36  10939  decbin3  10947  fac3  12145  hash3  12252  hashtplei  12273  hashtpg  12274  s3len  12606  repsw3  12639  3exp3  14206  13prm  14231  37prm  14236  43prm  14237  83prm  14238  139prm  14239  163prm  14240  317prm  14241  631prm  14242  1259lem1  14243  1259lem2  14244  1259lem4  14246  1259lem5  14247  1259prm  14248  2503lem2  14250  2503prm  14252  4001lem1  14253  4001lem2  14254  4001lem4  14256  4001prm  14257  dcubic1lem  22340  dcubic2  22341  mcubic  22344  log2ublem3  22445  log2ub  22446  birthday  22450  chtub  22653  3v3e3cycl1  23651  constr3trllem5  23661  4cycl4v4e  23673  4cycl4dv4e  23675  fib3  26906  halfthird  27512  bpoly3  28321  bpoly4  28322  jm2.23  29469  wallispilem4  29987  wallispi2lem1  29990  stirlinglem11  30003  f13idfv  30272  cnm2m1cnm3  30303  prmn2uzge3  30373  extwwlkfablem2  30795  numclwwlkovf2ex  30803  frgraregord013  30835  pgrpgt2nabel  30895
  Copyright terms: Public domain W3C validator