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

Theorem 1p1e2 10656
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 10601 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2456 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383  (class class class)co 6281   1c1 9496    + caddc 9498   2c2 10592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-2 10601
This theorem is referenced by:  2m1e1  10657  add1p1  10795  sub1m1  10796  nn0n0n1ge2  10866  10p10e20  11056  5t4e20  11061  6t4e24  11065  7t3e21  11069  8t3e24  11075  9t3e27  11082  fac2  12341  hash2  12452  hashprlei  12496  ccat2s1len  12610  ccat2s1p2  12615  ccatw2s1p2  12623  s2len  12834  repsw2  12870  swrd2lsw  12872  2swrd2eqwrdeq  12873  2exp8  14556  2exp16  14557  prmlem0  14573  prmlem2  14587  37prm  14588  43prm  14589  83prm  14590  317prm  14593  631prm  14594  1259lem1  14595  1259lem2  14596  1259lem4  14598  1259lem5  14599  2503lem1  14601  2503lem2  14602  2503lem3  14603  2503prm  14604  4001lem2  14606  4001lem3  14607  4001lem4  14608  m2detleiblem2  19108  iblcnlem1  22172  log2ublem3  23257  log2ub  23258  1sgm2ppw  23453  2sqb  23631  rplogsumlem2  23648  tgldimor  23871  wlkntrllem2  24540  2wlklem  24544  wlkdvspthlem  24587  3v3e3cycl1  24622  constr3trllem5  24632  constr3pthlem1  24633  constr3pthlem3  24635  wwlkextwrd  24706  wwlkextproplem3  24721  clwlkisclwwlklem2a4  24762  clwlkisclwwlklem2a  24763  clwwlkext2edg  24780  wwlkext2clwwlk  24781  nbhashuvtx1  24893  rusgranumwlkl1  24925  numclwlk1lem2fo  25073  numclwlk2lem2f  25081  archirngz  27711  archiabllem2c  27717  logblt  28000  fiblem  28315  fibp1  28318  fib2  28319  fib3  28320  ballotlem2  28405  ballotlemfc0  28409  ballotlemfcc  28410  signstfveq0  28512  subfacp1lem5  28606  rabren3dioph  30725  areaquad  31160  sumnnodd  31590  itgsin0pilem1  31702  itgsinexp  31707  stoweidlem14  31750  stoweidlem26  31762  wallispilem3  31803  stirlinglem6  31815  stirlinglem11  31820  dirkertrigeqlem1  31834  sqwvfourb  31966  fourierswlem  31967  oddinmgm  32456
  Copyright terms: Public domain W3C validator