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

Theorem 1p1e2 9840
Description: One plus one equals two. (Contributed by NM, 1-Apr-2008.)
Assertion
Ref Expression
1p1e2  |-  ( 1  +  1 )  =  2

Proof of Theorem 1p1e2
StepHypRef Expression
1 df-2 9804 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2287 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5858   1c1 8738    + caddc 8740   2c2 9795
This theorem is referenced by:  2m1e1  9841  1mhlfehlf  9934  addltmul  9947  zeo  10097  10p10e20  10194  5t4e20  10199  6t4e24  10203  7t3e21  10207  8t3e24  10213  9t3e27  10220  fac2  11294  bcn2  11331  hash2  11371  hashprlei  11379  s2len  11537  geo2sum2  12330  cos2tsin  12459  odd2np1  12587  oddp1even  12589  prmdiv  12853  2exp8  13102  2exp16  13103  prmlem0  13107  prmlem2  13121  37prm  13122  43prm  13123  83prm  13124  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem4  13132  1259lem5  13133  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem2  13140  4001lem3  13141  4001lem4  13142  htpycc  18478  pco1  18513  pcohtpylem  18517  pcopt  18520  pcorevlem  18524  iblcnlem1  19142  cos2pi  19844  atans2  20227  log2ublem3  20244  log2ub  20245  ppiprm  20389  ppinprm  20390  chtprm  20391  chtnprm  20392  1sgm2ppw  20439  lgslem4  20538  lgseisenlem1  20588  2sqb  20617  rplogsumlem1  20633  rplogsumlem2  20634  logdivsum  20682  log2sumbnd  20693  ex-fl  20834  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  logblt  23408  coinflippvt  23685  subfacp1lem5  23715  axlowdim  24589  bpoly2  24792  bpoly4  24794  fsumcube  24795  intset  26044  rabren3dioph  26898  lhe4.4ex1a  27546  itgsin0pilem1  27744  itgsinexp  27749  stoweidlem14  27763  stoweidlem26  27775  wallispilem3  27816  stirlinglem6  27828  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-2 9804
  Copyright terms: Public domain W3C validator