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

Theorem 1p1e2 11404
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 11335 . 2 2 = (1 + 1)
21eqcomi 2774 1 (1 + 1) = 2
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  (class class class)co 6842  1c1 10190   + caddc 10192  2c2 11327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-2 11335
This theorem is referenced by:  2m1e1  11405  add1p1  11529  sub1m1  11530  nn0n0n1ge2  11605  3halfnz  11703  10p10e20  11836  5t4e20  11843  6t4e24  11847  7t3e21  11851  8t3e24  11857  9t3e27  11864  fz0to3un2pr  12649  fzo13pr  12760  fzo1to4tp  12764  fldiv4p1lem1div2  12844  m1modge3gt1  12925  fac2  13270  hash2  13394  hashprlei  13451  ccat2s1len  13596  ccat2s1p2  13604  s2len  13920  repsw2  13981  swrd2lsw  13983  2swrd2eqwrdeq  13984  2swrd2eqwrdeqOLD  13985  nn0o1gt2  15381  3lcm2e6woprm  15611  2exp8  16072  2exp16  16073  prmlem0  16088  prmlem2  16102  37prm  16103  43prm  16104  83prm  16105  317prm  16108  631prm  16109  1259lem1  16113  1259lem2  16114  1259lem4  16116  1259lem5  16117  2503lem1  16119  2503lem2  16120  2503lem3  16121  2503prm  16122  4001lem2  16124  4001lem3  16125  4001lem4  16126  m2detleiblem2  20711  iblcnlem1  23845  logbleb  24812  logblt  24813  log2ublem3  24966  log2ub  24967  1sgm2ppw  25216  2sqb  25448  rplogsumlem2  25465  tgldimor  25688  1loopgrvd2  26690  2wlklem  26854  pthdlem1  26953  pthdlem2  26955  wwlksnextwrd  27097  wwlksnextproplem3  27112  2wlkdlem5  27132  2wlkdlem10  27138  rusgrnumwwlkl1  27173  clwlkclwwlklem2a4  27203  clwlkclwwlklem2a  27204  clwwlkext2edg  27269  wwlksext2clwwlk  27270  wwlksext2clwwlkOLD  27271  clwlknf1oclwwlknlem1  27308  3wlkdlem5  27399  3wlkdlem10  27405  upgr3v3e3cycl  27416  upgr4cycl4dv4e  27421  konigsberglem1  27488  konigsberglem2  27489  konigsberglem3  27490  numclwlk2lem2f  27620  numclwlk2lem2fOLD  27627  ex-exp  27701  archirngz  30125  archiabllem2c  30131  psgnfzto1st  30237  lmat22e12  30267  lmat22e21  30268  lmat22e22  30269  madjusmdetlem4  30278  fiblem  30843  fibp1  30846  fib2  30847  fib3  30848  ballotlem2  30933  ballotlemfc0  30937  ballotlemfcc  30938  signstfveq0  31037  chtvalz  31090  hgt750lem  31112  hgt750lem2  31113  subfacp1lem5  31546  dnibndlem13  32851  knoppndvlem12  32885  rabren3dioph  37989  pellfundgt1  38057  areaquad  38410  trclfvdecomr  38627  xralrple2  40140  sumnnodd  40432  itgsin0pilem1  40735  itgsinexp  40740  stoweidlem14  40800  stoweidlem26  40812  wallispilem3  40853  stirlinglem6  40865  stirlinglem11  40870  dirkertrigeqlem1  40884  sqwvfourb  41015  fourierswlem  41016  fmtno5lem1  42073  fmtno5lem4  42076  257prm  42081  fmtnoprmfac1lem  42084  fmtnofac1  42090  127prm  42123  2exp11  42125  m11nprm  42126  lighneallem2  42131  proththd  42139  opoeALTV  42202  1oddALTV  42209  nnsum3primes4  42284  nnsum3primesgbe  42288  nnsum4primesodd  42292  nnsum4primesoddALTV  42293  bgoldbtbndlem1  42301  oddinmgm  42416  fldivexpfllog2  42960  blen2  42980
  Copyright terms: Public domain W3C validator