Theorem 1p1e2 12383

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11120   + caddc 11122  2c2 12314

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 2156  ax-ext 2737

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

This theorem is used by:  2m1e1OLD  12385  1p2e3  12402  add1p1  12514  sub1m1  12515  nn0n0n1ge2  12591  3halfnz  12695  10p10e20  12831  5t4e20  12838  6t4e24  12842  7t3e21  12846  8t3e24  12852  9t3e27  12859  fz12pr  13630  fz0to3un2pr  13678  fzo13pr  13799  fzo1to4tp  13804  fldiv4p1lem1div2  13890  m1modge3gt1  13976  fac2  14337  hash2  14463  hashprlei  14527  ccat2s1len  14685  ccat2s1p2  14692  s2len  14954  repsw2  15015  swrd2lsw  15017  2swrd2eqwrdeq  15018  nn0o1gt2  16465  3lcm2e6woprm  16699  ge2nprmge4  16786  2exp8  17174  2exp11  17175  2exp16  17176  prmlem0  17191  prmlem2  17206  37prm  17207  43prm  17208  83prm  17209  317prm  17212  631prm  17213  1259lem1  17217  1259lem2  17218  1259lem4  17220  1259lem5  17221  2503lem1  17223  2503lem2  17224  2503lem3  17225  2503prm  17226  4001lem2  17228  4001lem3  17229  4001lem4  17230  m2detleiblem2  22839  logbleb  27003  logblt  27004  log2ublem3  27168  log2ub  27169  1sgm2ppw  27419  2sqb  27651  2sq2  27652  rplogsumlem2  27704  tgldimor  28826  1loopgrvd2  29915  2wlklem  30077  pthdlem1  30183  pthdlem2  30185  wwlksnextwrd  30317  wwlksnextproplem3  30331  2wlkdlem5  30349  2wlkdlem10  30355  rusgrnumwwlkl1  30391  clwlkclwwlklem2a4  30419  clwlkclwwlklem2a  30420  clwwlkext2edg  30478  wwlksext2clwwlk  30479  clwlknf1oclwwlknlem1  30503  3wlkdlem5  30589  3wlkdlem10  30595  upgr3v3e3cycl  30606  upgr4cycl4dv4e  30611  konigsberglem1  30678  konigsberglem2  30679  konigsberglem3  30680  numclwlk2lem2f  30803  ex-exp  30876  1nei  33156  psgnfzto1st  33493  cyc3fv2  33526  archirngz  33577  archiabllem2c  33583  cos9thpiminplylem1  34240  lmat22e12  34277  lmat22e21  34278  lmat22e22  34279  madjusmdetlem4  34288  fiblem  34857  fibp1  34860  fib2  34861  fib3  34862  ballotlem2  34948  ballotlemfc0  34952  ballotlemfcc  34953  signstfveq0  35033  chtvalz  35085  hgt750lem  35107  hgt750lem2  35108  subfacp1lem5  35717  dnibndlem13  37140  knoppndvlem12  37173  420gcd8e4  42835  3exp7  42882  3lexlogpow5ineq1  42883  aks4d1p1  42905  2np3bcnp1  42973  sn-0ne2  43244  flt0  43446  fltnltalem  43471  rabren3dioph  43619  pellfundgt1  43687  areaquad  44020  resqrtvalex  44448  imsqrtvalex  44449  trclfvdecomr  44531  xralrple2  46147  sumnnodd  46423  itgsin0pilem1  46741  itgsinexp  46746  stoweidlem14  46805  stoweidlem26  46817  wallispilem3  46858  stirlinglem6  46870  stirlinglem11  46875  dirkertrigeqlem1  46889  sqwvfourb  47020  fourierswlem  47021  addmodne  48164  fmtno5lem1  48382  fmtno5lem4  48385  257prm  48390  fmtnoprmfac1lem  48393  fmtnofac1  48399  127prm  48428  m11nprm  48430  lighneallem2  48435  proththd  48443  opoeALTV  48525  1oddALTV  48532  nnsum3primes4  48630  nnsum3primesgbe  48634  nnsum4primesodd  48638  nnsum4primesoddALTV  48639  bgoldbtbndlem1  48647  grtriclwlk3  48787  cycl3grtrilem  48788  gpgprismgr4cycllem10  48946  oddinmgm  49016  fldivexpfllog2  49421  blen2  49441  ackval1  49537  ackval0012  49545  crosspdotsumlem  50722  crosspaltd  50724  crossp3d  50725