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

Theorem 1p1e2 9856
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 9820 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2300 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874   1c1 8754    + caddc 8756   2c2 9811
This theorem is referenced by:  2m1e1  9857  1mhlfehlf  9950  addltmul  9963  zeo  10113  10p10e20  10210  5t4e20  10215  6t4e24  10219  7t3e21  10223  8t3e24  10229  9t3e27  10236  fac2  11310  bcn2  11347  hash2  11387  hashprlei  11395  s2len  11553  geo2sum2  12346  cos2tsin  12475  odd2np1  12603  oddp1even  12605  prmdiv  12869  2exp8  13118  2exp16  13119  prmlem0  13123  prmlem2  13137  37prm  13138  43prm  13139  83prm  13140  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem4  13148  1259lem5  13149  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem2  13156  4001lem3  13157  4001lem4  13158  htpycc  18494  pco1  18529  pcohtpylem  18533  pcopt  18536  pcorevlem  18540  iblcnlem1  19158  cos2pi  19860  atans2  20243  log2ublem3  20260  log2ub  20261  ppiprm  20405  ppinprm  20406  chtprm  20407  chtnprm  20408  1sgm2ppw  20455  lgslem4  20554  lgseisenlem1  20604  2sqb  20633  rplogsumlem1  20649  rplogsumlem2  20650  logdivsum  20698  log2sumbnd  20709  ex-fl  20850  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  logblt  23423  coinflippvt  23700  subfacp1lem5  23730  axlowdim  24661  bpoly2  24864  bpoly4  24866  fsumcube  24867  intset  26147  rabren3dioph  27001  lhe4.4ex1a  27649  itgsin0pilem1  27847  itgsinexp  27852  stoweidlem14  27866  stoweidlem26  27878  wallispilem3  27919  stirlinglem6  27931  stirlinglem11  27936  wlkntrllem4  28348  wlkdvspthlem  28365  usgrcyclnl2  28387  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-2 9820
  Copyright terms: Public domain W3C validator