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

Theorem 2p1e3 10105
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 10061 . 2  |-  3  =  ( 2  +  1 )
21eqcomi 2442 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff set class
Syntax hints:    = wceq 1653  (class class class)co 6083   1c1 8993    + caddc 8995   2c2 10051   3c3 10052
This theorem is referenced by:  6t5e30  10464  7t5e35  10469  8t4e32  10474  9t4e36  10481  decbin3  10489  binom3  11502  fac3  11575  hash3  11677  hashtplei  11692  hashtpg  11693  s3len  11857  2exp16  13426  3exp3  13427  prmlem1a  13431  13prm  13440  23prm  13443  prmlem2  13444  37prm  13445  43prm  13446  83prm  13447  139prm  13448  163prm  13449  317prm  13450  631prm  13451  1259lem1  13452  1259lem2  13453  1259lem3  13454  1259lem4  13455  1259lem5  13456  1259prm  13457  2503lem2  13459  2503lem3  13460  2503prm  13461  4001lem1  13462  4001lem2  13463  4001lem4  13465  4001prm  13466  dcubic1lem  20685  dcubic2  20686  mcubic  20689  quart1lem  20697  log2ublem3  20790  log2ub  20791  birthday  20795  chtub  20998  pntibndlem2  21287  3v3e3cycl1  21633  constr3trllem5  21643  4cycl4v4e  21655  4cycl4dv4e  21657  1kp2ke3k  21756  halfthird  25207  bpoly3  26106  bpoly4  26107  jm2.23  27069  wallispilem4  27795  wallispi2lem1  27798  stirlinglem11  27811  f13idfv  28088
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-3 10061
  Copyright terms: Public domain W3C validator