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

Theorem 1p1e2 10640
Description: 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
Assertion
Ref Expression
1p1e2  |-  ( 1  +  1 )  =  2

Proof of Theorem 1p1e2
StepHypRef Expression
1 df-2 10585 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2475 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374  (class class class)co 6277   1c1 9484    + caddc 9486   2c2 10576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-cleq 2454  df-2 10585
This theorem is referenced by:  2m1e1  10641  add1p1  10779  sub1m1  10780  nn0n0n1ge2  10850  10p10e20  11037  5t4e20  11042  6t4e24  11046  7t3e21  11050  8t3e24  11056  9t3e27  11063  fac2  12316  hash2  12425  hashprlei  12469  ccat2s1len  12580  ccat2s1p2  12585  ccatw2s1p2  12593  s2len  12804  repsw2  12840  swrd2lsw  12842  2swrd2eqwrdeq  12843  2exp8  14423  2exp16  14424  prmlem0  14440  prmlem2  14454  37prm  14455  43prm  14456  83prm  14457  317prm  14460  631prm  14461  1259lem1  14462  1259lem2  14463  1259lem4  14465  1259lem5  14466  2503lem1  14468  2503lem2  14469  2503lem3  14470  2503prm  14471  4001lem2  14473  4001lem3  14474  4001lem4  14475  m2detleiblem2  18892  iblcnlem1  21924  log2ublem3  23002  log2ub  23003  1sgm2ppw  23198  2sqb  23376  rplogsumlem2  23393  tgldimor  23616  wlkntrllem2  24226  2wlklem  24230  wlkdvspthlem  24273  usgra2wlkspthlem1  24283  usgrcyclnl2  24305  3v3e3cycl1  24308  constr3trllem5  24318  constr3pthlem1  24319  constr3pthlem3  24321  4cycl4v4e  24330  4cycl4dv4e  24332  wwlkextwrd  24392  wwlkextproplem3  24407  clwlkisclwwlklem2a1  24443  clwlkisclwwlklem2a4  24448  clwlkisclwwlklem2a  24449  clwwlkext2edg  24466  wwlkext2clwwlk  24467  nbhashuvtx1  24579  rusgranumwlkl1  24611  numclwlk1lem2fo  24760  numclwlk2lem2f  24768  archirngz  27383  archiabllem2c  27389  logblt  27650  fiblem  27965  fibp1  27968  fib2  27969  fib3  27970  ballotlem2  28055  ballotlemfc0  28059  ballotlemfcc  28060  signstfveq0  28162  subfacp1lem5  28256  rabren3dioph  30342  areaquad  30780  sumnnodd  31129  itgsin0pilem1  31224  itgsinexp  31229  stoweidlem14  31271  stoweidlem26  31283  wallispilem3  31324  stirlinglem6  31336  stirlinglem11  31341  fourierdlem42  31406  sqwvfourb  31487  fourierswlem  31488  usgra2pthspth  31777  usgra2pthlem1  31779  usgra2pth  31780
  Copyright terms: Public domain W3C validator