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

Theorem 1p1e2 10434
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 10379 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2446 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369  (class class class)co 6090   1c1 9282    + caddc 9284   2c2 10370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-2 10379
This theorem is referenced by:  2m1e1  10435  sub1m1  10573  nn0n0n1ge2  10642  10p10e20  10824  5t4e20  10829  6t4e24  10833  7t3e21  10837  8t3e24  10843  9t3e27  10850  fac2  12056  hash2  12162  hashprlei  12176  s2len  12513  repsw2  12549  swrd2lsw  12551  2swrd2eqwrdeq  12552  2exp8  14115  2exp16  14116  prmlem0  14132  prmlem2  14146  37prm  14147  43prm  14148  83prm  14149  317prm  14152  631prm  14153  1259lem1  14154  1259lem2  14155  1259lem4  14157  1259lem5  14158  2503lem1  14160  2503lem2  14161  2503lem3  14162  2503prm  14163  4001lem2  14165  4001lem3  14166  4001lem4  14167  m2detleiblem2  18433  iblcnlem1  21264  log2ublem3  22342  log2ub  22343  1sgm2ppw  22538  2sqb  22716  rplogsumlem2  22733  tgldimor  22954  wlkntrllem2  23458  2wlklem  23462  wlkdvspthlem  23505  usgrcyclnl2  23526  3v3e3cycl1  23529  constr3trllem5  23539  constr3pthlem1  23540  constr3pthlem3  23542  4cycl4v4e  23551  4cycl4dv4e  23553  archirngz  26205  archiabllem2c  26211  logblt  26464  fiblem  26780  fibp1  26783  fib2  26784  fib3  26785  ballotlem2  26870  ballotlemfc0  26874  ballotlemfcc  26875  signstfveq0  26977  subfacp1lem5  27071  rabren3dioph  29152  areaquad  29590  itgsin0pilem1  29788  itgsinexp  29793  stoweidlem14  29807  stoweidlem26  29819  wallispilem3  29860  stirlinglem6  29872  stirlinglem11  29877  add1p1  30178  elfzom1elfzo  30215  ccat2s1len  30262  ccat2s1p2  30264  ccatw2s1p2  30268  usgra2pthspth  30293  usgra2wlkspthlem1  30294  usgra2pthlem1  30298  usgra2pth  30299  wwlkextwrd  30358  clwlkisclwwlklem2a1  30439  clwlkisclwwlklem2a4  30444  clwlkisclwwlklem2a  30445  clwwlkext2edg  30462  wwlkext2clwwlk  30463  nbhashuvtx1  30531  rusgranumwlkl1  30557  wwlkextproplem3  30560  numclwlk1lem2fo  30686  numclwlk2lem2f  30694
  Copyright terms: Public domain W3C validator