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

Theorem 1p1e2 10983
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 10928 . 2 2 = (1 + 1)
21eqcomi 2618 1 (1 + 1) = 2
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6526  1c1 9793   + caddc 9795  2c2 10919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-2 10928
This theorem is referenced by:  2m1e1  10984  add1p1  11132  sub1m1  11133  nn0n0n1ge2  11207  3halfnz  11290  10p10e20  11462  10p10e20OLD  11463  5t4e20  11471  5t4e20OLD  11472  6t4e24  11477  7t3e21  11483  8t3e24  11489  9t3e27  11498  fz0to3un2pr  12267  fzo13pr  12376  fzo1to4tp  12380  fldiv4p1lem1div2  12455  m1modge3gt1  12536  fac2  12885  hash2  13008  hashprlei  13061  ccat2s1len  13201  ccat2s1p2  13206  s2len  13432  repsw2  13489  swrd2lsw  13491  2swrd2eqwrdeq  13492  nn0o1gt2  14883  3lcm2e6woprm  15114  2exp8  15582  2exp16  15583  prmlem0  15598  prmlem2  15613  37prm  15614  43prm  15615  83prm  15616  317prm  15619  631prm  15620  1259lem1  15624  1259lem2  15625  1259lem4  15627  1259lem5  15628  2503lem1  15630  2503lem2  15631  2503lem3  15632  2503prm  15633  4001lem2  15635  4001lem3  15636  4001lem4  15637  m2detleiblem2  20200  iblcnlem1  23304  logbleb  24265  logblt  24266  log2ublem3  24419  log2ub  24420  1sgm2ppw  24669  2sqb  24901  rplogsumlem2  24918  tgldimor  25141  wlkntrllem2  25883  2wlklem  25887  wlkdvspthlem  25930  3v3e3cycl1  25965  constr3trllem5  25975  constr3pthlem1  25976  constr3pthlem3  25978  wwlkextwrd  26049  wwlkextproplem3  26064  clwlkisclwwlklem2a4  26105  clwlkisclwwlklem2a  26106  clwwlkext2edg  26123  wwlkext2clwwlk  26124  nbhashuvtx1  26235  rusgranumwlkl1  26267  numclwlk1lem2fo  26415  numclwlk2lem2f  26423  ex-exp  26492  archirngz  28867  archiabllem2c  28873  psgnfzto1st  28979  lmat22e12  29006  lmat22e21  29007  lmat22e22  29008  madjusmdetlem4  29017  fiblem  29580  fibp1  29583  fib2  29584  fib3  29585  ballotlem2  29670  ballotlemfc0  29674  ballotlemfcc  29675  signstfveq0  29773  subfacp1lem5  30213  dnibndlem13  31443  knoppndvlem12  31477  rabren3dioph  36180  pellfundgt1  36248  areaquad  36604  trclfvdecomr  36822  xralrple2  38294  sumnnodd  38480  itgsin0pilem1  38624  itgsinexp  38629  stoweidlem14  38690  stoweidlem26  38702  wallispilem3  38743  stirlinglem6  38755  stirlinglem11  38760  dirkertrigeqlem1  38774  sqwvfourb  38905  fourierswlem  38906  fmtno5lem1  39787  fmtno5lem4  39790  257prm  39795  fmtnoprmfac1lem  39798  fmtnofac1  39804  127prm  39837  2exp11  39839  m11nprm  39840  lighneallem2  39845  proththd  39853  opoeALTV  39916  1oddALTV  39923  nnsum3primes4  39988  nnsum3primesgbe  39992  nnsum4primesodd  39996  nnsum4primesoddALTV  39997  bgoldbtbndlem1  40005  1loopgrvd2  40699  2Wlklem  40856  usgr2wlkneq  40943  usgr2trlncl  40947  pthdlem1  40953  pthdlem2  40955  wwlksnextwrd  41084  wwlksnextproplem3  41098  21wlkdlem5  41117  21wlkdlem10  41123  rusgrnumwwlkl1  41153  clwlkclwwlklem2a4  41187  clwlkclwwlklem2a  41188  clwwlksext2edg  41211  wwlksext2clwwlk  41212  31wlkdlem5  41311  31wlkdlem10  41317  upgr3v3e3cycl  41328  upgr4cycl4dv4e  41333  konigsberglem1  41403  konigsberglem2  41404  konigsberglem3  41405  av-numclwlk1lem2fo  41506  av-numclwlk2lem2f  41514  oddinmgm  41586  fldivexpfllog2  42138  blen2  42158
  Copyright terms: Public domain W3C validator