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

Theorem 1p1e2 10566
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 10511 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2395 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff setvar class
Syntax hints:    = wceq 1399  (class class class)co 6196   1c1 9404    + caddc 9406   2c2 10502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-cleq 2374  df-2 10511
This theorem is referenced by:  2m1e1  10567  add1p1  10705  sub1m1  10706  nn0n0n1ge2  10776  10p10e20  10965  5t4e20  10970  6t4e24  10974  7t3e21  10978  8t3e24  10984  9t3e27  10991  fac2  12261  hash2  12374  hashprlei  12418  ccat2s1len  12537  ccat2s1p2  12542  s2len  12763  repsw2  12799  swrd2lsw  12801  2swrd2eqwrdeq  12802  2exp8  14576  2exp16  14577  prmlem0  14593  prmlem2  14607  37prm  14608  43prm  14609  83prm  14610  317prm  14613  631prm  14614  1259lem1  14615  1259lem2  14616  1259lem4  14618  1259lem5  14619  2503lem1  14621  2503lem2  14622  2503lem3  14623  2503prm  14624  4001lem2  14626  4001lem3  14627  4001lem4  14628  m2detleiblem2  19215  iblcnlem1  22279  logbleb  23241  logblt  23242  log2ublem3  23395  log2ub  23396  1sgm2ppw  23592  2sqb  23770  rplogsumlem2  23787  tgldimor  24013  wlkntrllem2  24683  2wlklem  24687  wlkdvspthlem  24730  3v3e3cycl1  24765  constr3trllem5  24775  constr3pthlem1  24776  constr3pthlem3  24778  wwlkextwrd  24849  wwlkextproplem3  24864  clwlkisclwwlklem2a4  24905  clwlkisclwwlklem2a  24906  clwwlkext2edg  24923  wwlkext2clwwlk  24924  nbhashuvtx1  25036  rusgranumwlkl1  25068  numclwlk1lem2fo  25216  numclwlk2lem2f  25224  archirngz  27886  archiabllem2c  27892  fiblem  28520  fibp1  28523  fib2  28524  fib3  28525  ballotlem2  28610  ballotlemfc0  28614  ballotlemfcc  28615  signstfveq0  28717  subfacp1lem5  28817  rabren3dioph  30914  areaquad  31352  sumnnodd  31802  itgsin0pilem1  31914  itgsinexp  31919  stoweidlem14  31962  stoweidlem26  31974  wallispilem3  32015  stirlinglem6  32027  stirlinglem11  32032  dirkertrigeqlem1  32046  sqwvfourb  32178  fourierswlem  32179  opoeALTV  32525  1oddALTV  32532  proththd  32548  oddinmgm  32821  3halfnz  33326  nn0o1gt2  33337  fldivexpfllog2  33386  blen2  33406
  Copyright terms: Public domain W3C validator