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

Theorem 2p1e3 9847
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 9805 . 2  |-  3  =  ( 2  +  1 )
21eqcomi 2287 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5858   1c1 8738    + caddc 8740   2c2 9795   3c3 9796
This theorem is referenced by:  6t5e30  10204  7t5e35  10209  8t4e32  10214  9t4e36  10221  decbin3  10229  binom3  11222  fac3  11295  hash3  11372  hashtplei  11380  s3len  11541  3prm  12775  2exp16  13103  3exp3  13104  prmlem1a  13108  13prm  13117  23prm  13120  prmlem2  13121  37prm  13122  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem4  13142  4001prm  13143  1cubrlem  20137  1cubr  20138  dcubic1lem  20139  dcubic2  20140  mcubic  20143  quart1lem  20151  quart1  20152  log2ublem3  20244  log2ub  20245  birthday  20249  pntibndlem2  20740  1kp2ke3k  20833  halfthird  24100  bpoly3  24793  bpoly4  24794  cntrset  25602  jm2.23  27089  lhe4.4ex1a  27546  wallispilem4  27817  wallispi2lem1  27820  stirlinglem11  27833
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-3 9805
  Copyright terms: Public domain W3C validator