Theorem 1p1e2 12466

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420  1c1 11201   + caddc 11203  2c2 12397

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-2 12405

This theorem is used by:  2m1e1OLD  12468  1p2e3  12485  add1p1  12597  sub1m1  12598  nn0n0n1ge2  12674  3halfnz  12778  10p10e20  12914  5t4e20  12921  6t4e24  12925  7t3e21  12929  8t3e24  12935  9t3e27  12942  fz12pr  13715  fz0to3un2pr  13763  fzo13pr  13884  fzo1to4tp  13889  fldiv4p1lem1div2  13975  m1modge3gt1  14061  fac2  14423  hash2  14549  hashprlei  14613  ccat2s1len  14771  ccat2s1p2  14778  s2len  15040  repsw2  15103  swrd2lsw  15105  2swrd2eqwrdeq  15106  nn0o1gt2  16551  3lcm2e6woprm  16790  ge2nprmge4  16877  2exp8  17266  2exp11  17267  2exp16  17268  prmlem0  17283  prmlem2  17298  37prm  17299  43prm  17300  83prm  17301  317prm  17304  631prm  17305  1259lem1  17309  1259lem2  17310  1259lem4  17312  1259lem5  17313  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem2  17320  4001lem3  17321  4001lem4  17322  m2detleiblem2  22943  logbleb  27111  logblt  27112  log2ublem3  27276  log2ub  27277  1sgm2ppw  27527  2sqb  27759  2sq2  27760  rplogsumlem2  27812  flt0  27969  tgldimor  28965  1loopgrvd2  30084  2wlklem  30246  pthdlem1  30352  pthdlem2  30354  wwlksnextwrd  30486  wwlksnextproplem3  30500  2wlkdlem5  30518  2wlkdlem10  30524  rusgrnumwwlkl1  30560  clwlkclwwlklem2a4  30588  clwlkclwwlklem2a  30589  clwwlkext2edg  30647  wwlksext2clwwlk  30648  clwlknf1oclwwlknlem1  30672  3wlkdlem5  30764  3wlkdlem10  30770  upgr3v3e3cycl  30781  upgr4cycl4dv4e  30786  konigsberglem1  30853  konigsberglem2  30854  konigsberglem3  30855  numclwlk2lem2f  30978  ex-exp  31051  1nei  33329  psgnfzto1st  33666  cyc3fv2  33699  archirngz  33750  archiabllem2c  33756  cos9thpiminplylem1  34414  lmat22e12  34451  lmat22e21  34452  lmat22e22  34453  madjusmdetlem4  34462  fiblem  35030  fibp1  35033  fib2  35034  fib3  35035  ballotlem2  35121  ballotlemfc0  35125  ballotlemfcc  35126  signstfveq0  35206  chtvalz  35258  hgt750lem  35280  hgt750lem2  35281  subfacp1lem5  35949  dnibndlem13  37356  knoppndvlem12  37389  420gcd8e4  43056  3exp7  43103  3lexlogpow5ineq1  43104  aks4d1p1  43126  2np3bcnp1  43194  sn-0ne2  43457  fltnltalem  43673  rabren3dioph  43821  pellfundgt1  43889  areaquad  44217  resqrtvalex  44644  imsqrtvalex  44645  trclfvdecomr  44727  xralrple2  46365  sumnnodd  46641  itgsin0pilem1  46959  itgsinexp  46964  stoweidlem14  47023  stoweidlem26  47035  wallispilem3  47076  stirlinglem6  47088  stirlinglem11  47093  dirkertrigeqlem1  47107  sqwvfourb  47238  fourierswlem  47239  addmodne  48419  fmtno5lem1  48637  fmtno5lem4  48640  257prm  48645  fmtnoprmfac1lem  48648  fmtnofac1  48654  127prm  48683  m11nprm  48685  lighneallem2  48690  proththd  48698  opoeALTV  48780  1oddALTV  48787  nnsum3primes4  48885  nnsum3primesgbe  48889  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  bgoldbtbndlem1  48902  grtriclwlk3  49042  cycl3grtrilem  49043  gpgprismgr4cycllem10  49201  oddinmgm  49271  fldivexpfllog2  49676  blen2  49696  ackval1  49792  ackval0012  49800  crosspdotsumlem  50963  crosspaltd  50965  crossp3d  50966  veronesevrowd  50978  veroquadgsumlem  50982