Theorem 1p1e2 12107

Description: 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)

Assertion

Ref	Expression
1p1e2	⊢ (1 + 1) = 2

Proof of Theorem 1p1e2

Step	Hyp	Ref	Expression
1		df-2 12045	. 2 ⊢ 2 = (1 + 1)
2	1	eqcomi 2748	1 ⊢ (1 + 1) = 2

Syntax hints:   = wceq 1539  (class class class)co 7284  1c1 10881   + caddc 10883  2c2 12037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-2 12045

This theorem is referenced by:  2m1e1  12108  1p2e3  12125  add1p1  12233  sub1m1  12234  nn0n0n1ge2  12309  3halfnz  12408  10p10e20  12541  5t4e20  12548  6t4e24  12552  7t3e21  12556  8t3e24  12562  9t3e27  12569  fz12pr  13322  fz0to3un2pr  13367  fzo13pr  13480  fzo1to4tp  13484  fldiv4p1lem1div2  13564  m1modge3gt1  13647  fac2  14002  hash2  14129  hashprlei  14191  ccat2s1len  14337  ccat2s1lenOLD  14338  ccat2s1p2  14346  ccat2s1p2OLD  14348  s2len  14611  repsw2  14672  swrd2lsw  14674  2swrd2eqwrdeq  14675  nn0o1gt2  16099  3lcm2e6woprm  16329  ge2nprmge4  16415  2exp8  16799  2exp11  16800  2exp16  16801  prmlem0  16816  prmlem2  16830  37prm  16831  43prm  16832  83prm  16833  317prm  16836  631prm  16837  1259lem1  16841  1259lem2  16842  1259lem4  16844  1259lem5  16845  2503lem1  16847  2503lem2  16848  2503lem3  16849  2503prm  16850  4001lem2  16852  4001lem3  16853  4001lem4  16854  m2detleiblem2  21786  logbleb  25942  logblt  25943  log2ublem3  26107  log2ub  26108  1sgm2ppw  26357  2sqb  26589  2sq2  26590  rplogsumlem2  26642  tgldimor  26872  1loopgrvd2  27879  2wlklem  28044  pthdlem1  28143  pthdlem2  28145  wwlksnextwrd  28271  wwlksnextproplem3  28285  2wlkdlem5  28303  2wlkdlem10  28309  rusgrnumwwlkl1  28342  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwwlkext2edg  28429  wwlksext2clwwlk  28430  clwlknf1oclwwlknlem1  28454  3wlkdlem5  28536  3wlkdlem10  28542  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  konigsberglem1  28625  konigsberglem2  28626  konigsberglem3  28627  numclwlk2lem2f  28750  ex-exp  28823  1nei  31080  psgnfzto1st  31381  cyc3fv2  31414  archirngz  31452  archiabllem2c  31458  lmat22e12  31778  lmat22e21  31779  lmat22e22  31780  madjusmdetlem4  31789  fiblem  32374  fibp1  32377  fib2  32378  fib3  32379  ballotlem2  32464  ballotlemfc0  32468  ballotlemfcc  32469  signstfveq0  32565  chtvalz  32618  hgt750lem  32640  hgt750lem2  32641  subfacp1lem5  33155  dnibndlem13  34679  knoppndvlem12  34712  420gcd8e4  40021  3exp7  40068  3lexlogpow5ineq1  40069  aks4d1p1  40091  2np3bcnp1  40107  sn-0ne2  40396  flt0  40481  fltnltalem  40506  rabren3dioph  40644  pellfundgt1  40712  areaquad  41054  resqrtvalex  41260  imsqrtvalex  41261  trclfvdecomr  41343  xralrple2  42900  sumnnodd  43178  itgsin0pilem1  43498  itgsinexp  43503  stoweidlem14  43562  stoweidlem26  43574  wallispilem3  43615  stirlinglem6  43627  stirlinglem11  43632  dirkertrigeqlem1  43646  sqwvfourb  43777  fourierswlem  43778  fmtno5lem1  45016  fmtno5lem4  45019  257prm  45024  fmtnoprmfac1lem  45027  fmtnofac1  45033  127prm  45062  m11nprm  45064  lighneallem2  45069  proththd  45077  opoeALTV  45146  1oddALTV  45153  nnsum3primes4  45251  nnsum3primesgbe  45255  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  bgoldbtbndlem1  45268  oddinmgm  45380  fldivexpfllog2  45922  blen2  45942  ackval1  46038  ackval0012  46046