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

Theorem 2p1e3 9863
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 9821 . 2  |-  3  =  ( 2  +  1 )
21eqcomi 2300 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874   1c1 8754    + caddc 8756   2c2 9811   3c3 9812
This theorem is referenced by:  6t5e30  10220  7t5e35  10225  8t4e32  10230  9t4e36  10237  decbin3  10245  binom3  11238  fac3  11311  hash3  11388  hashtplei  11396  s3len  11557  3prm  12791  2exp16  13119  3exp3  13120  prmlem1a  13124  13prm  13133  23prm  13136  prmlem2  13137  37prm  13138  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem4  13158  4001prm  13159  1cubrlem  20153  1cubr  20154  dcubic1lem  20155  dcubic2  20156  mcubic  20159  quart1lem  20167  quart1  20168  log2ublem3  20260  log2ub  20261  birthday  20265  pntibndlem2  20756  1kp2ke3k  20849  halfthird  24115  bpoly3  24865  bpoly4  24866  itg2addnc  25005  cntrset  25705  jm2.23  27192  lhe4.4ex1a  27649  wallispilem4  27920  wallispi2lem1  27923  stirlinglem11  27936  hashtpg  28217  3v3e3cycl1  28390  constr3trllem5  28400  4cycl4v4e  28412  4cycl4dv4e  28414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-3 9821
  Copyright terms: Public domain W3C validator