Theorem 1p1e2 12391

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 12329	. 2 ⊢ 2 = (1 + 1)
2	1	eqcomi 2746	1 ⊢ (1 + 1) = 2

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  2c2 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-2 12329

This theorem is referenced by:  2m1e1  12392  1p2e3  12409  add1p1  12517  sub1m1  12518  nn0n0n1ge2  12594  3halfnz  12697  10p10e20  12828  5t4e20  12835  6t4e24  12839  7t3e21  12843  8t3e24  12849  9t3e27  12856  fz12pr  13621  fz0to3un2pr  13669  fzo13pr  13788  fzo1to4tp  13793  fldiv4p1lem1div2  13875  m1modge3gt1  13959  fac2  14318  hash2  14444  hashprlei  14507  ccat2s1len  14661  ccat2s1p2  14668  s2len  14928  repsw2  14989  swrd2lsw  14991  2swrd2eqwrdeq  14992  nn0o1gt2  16418  3lcm2e6woprm  16652  ge2nprmge4  16738  2exp8  17126  2exp11  17127  2exp16  17128  prmlem0  17143  prmlem2  17157  37prm  17158  43prm  17159  83prm  17160  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem2  17179  4001lem3  17180  4001lem4  17181  m2detleiblem2  22634  logbleb  26826  logblt  26827  log2ublem3  26991  log2ub  26992  1sgm2ppw  27244  2sqb  27476  2sq2  27477  rplogsumlem2  27529  tgldimor  28510  1loopgrvd2  29521  2wlklem  29685  pthdlem1  29786  pthdlem2  29788  wwlksnextwrd  29917  wwlksnextproplem3  29931  2wlkdlem5  29949  2wlkdlem10  29955  rusgrnumwwlkl1  29988  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwwlkext2edg  30075  wwlksext2clwwlk  30076  clwlknf1oclwwlknlem1  30100  3wlkdlem5  30182  3wlkdlem10  30188  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  numclwlk2lem2f  30396  ex-exp  30469  1nei  32747  psgnfzto1st  33125  cyc3fv2  33158  archirngz  33196  archiabllem2c  33202  lmat22e12  33818  lmat22e21  33819  lmat22e22  33820  madjusmdetlem4  33829  fiblem  34400  fibp1  34403  fib2  34404  fib3  34405  ballotlem2  34491  ballotlemfc0  34495  ballotlemfcc  34496  signstfveq0  34592  chtvalz  34644  hgt750lem  34666  hgt750lem2  34667  subfacp1lem5  35189  dnibndlem13  36491  knoppndvlem12  36524  420gcd8e4  42007  3exp7  42054  3lexlogpow5ineq1  42055  aks4d1p1  42077  2np3bcnp1  42145  sn-0ne2  42436  flt0  42647  fltnltalem  42672  rabren3dioph  42826  pellfundgt1  42894  areaquad  43228  resqrtvalex  43658  imsqrtvalex  43659  trclfvdecomr  43741  xralrple2  45365  sumnnodd  45645  itgsin0pilem1  45965  itgsinexp  45970  stoweidlem14  46029  stoweidlem26  46041  wallispilem3  46082  stirlinglem6  46094  stirlinglem11  46099  dirkertrigeqlem1  46113  sqwvfourb  46244  fourierswlem  46245  addmodne  47346  fmtno5lem1  47540  fmtno5lem4  47543  257prm  47548  fmtnoprmfac1lem  47551  fmtnofac1  47557  127prm  47586  m11nprm  47588  lighneallem2  47593  proththd  47601  opoeALTV  47670  1oddALTV  47677  nnsum3primes4  47775  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  bgoldbtbndlem1  47792  grtriclwlk3  47912  cycl3grtrilem  47913  oddinmgm  48091  fldivexpfllog2  48486  blen2  48506  ackval1  48602  ackval0012  48610