Theorem 1p1e2 12279

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

Syntax hints:   = wceq 1542  (class class class)co 7370  1c1 11041   + caddc 11043  2c2 12214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  2m1e1  12280  1p2e3  12297  add1p1  12406  sub1m1  12407  nn0n0n1ge2  12483  3halfnz  12585  10p10e20  12716  5t4e20  12723  6t4e24  12727  7t3e21  12731  8t3e24  12737  9t3e27  12744  fz12pr  13511  fz0to3un2pr  13559  fzo13pr  13679  fzo1to4tp  13684  fldiv4p1lem1div2  13769  m1modge3gt1  13855  fac2  14216  hash2  14342  hashprlei  14405  ccat2s1len  14561  ccat2s1p2  14568  s2len  14826  repsw2  14887  swrd2lsw  14889  2swrd2eqwrdeq  14890  nn0o1gt2  16322  3lcm2e6woprm  16556  ge2nprmge4  16642  2exp8  17030  2exp11  17031  2exp16  17032  prmlem0  17047  prmlem2  17061  37prm  17062  43prm  17063  83prm  17064  317prm  17067  631prm  17068  1259lem1  17072  1259lem2  17073  1259lem4  17075  1259lem5  17076  2503lem1  17078  2503lem2  17079  2503lem3  17080  2503prm  17081  4001lem2  17083  4001lem3  17084  4001lem4  17085  m2detleiblem2  22589  logbleb  26766  logblt  26767  log2ublem3  26931  log2ub  26932  1sgm2ppw  27184  2sqb  27416  2sq2  27417  rplogsumlem2  27469  tgldimor  28592  1loopgrvd2  29595  2wlklem  29757  pthdlem1  29857  pthdlem2  29859  wwlksnextwrd  29988  wwlksnextproplem3  30002  2wlkdlem5  30020  2wlkdlem10  30026  rusgrnumwwlkl1  30062  clwlkclwwlklem2a4  30090  clwlkclwwlklem2a  30091  clwwlkext2edg  30149  wwlksext2clwwlk  30150  clwlknf1oclwwlknlem1  30174  3wlkdlem5  30256  3wlkdlem10  30262  upgr3v3e3cycl  30273  upgr4cycl4dv4e  30278  konigsberglem1  30345  konigsberglem2  30346  konigsberglem3  30347  numclwlk2lem2f  30470  ex-exp  30543  1nei  32833  psgnfzto1st  33205  cyc3fv2  33238  archirngz  33289  archiabllem2c  33295  cos9thpiminplylem1  33966  lmat22e12  34003  lmat22e21  34004  lmat22e22  34005  madjusmdetlem4  34014  fiblem  34582  fibp1  34585  fib2  34586  fib3  34587  ballotlem2  34673  ballotlemfc0  34677  ballotlemfcc  34678  signstfveq0  34761  chtvalz  34813  hgt750lem  34835  hgt750lem2  34836  subfacp1lem5  35406  dnibndlem13  36718  knoppndvlem12  36751  420gcd8e4  42405  3exp7  42452  3lexlogpow5ineq1  42453  aks4d1p1  42475  2np3bcnp1  42543  sn-0ne2  42805  flt0  43024  fltnltalem  43049  rabren3dioph  43201  pellfundgt1  43269  areaquad  43602  resqrtvalex  44030  imsqrtvalex  44031  trclfvdecomr  44113  xralrple2  45742  sumnnodd  46019  itgsin0pilem1  46337  itgsinexp  46342  stoweidlem14  46401  stoweidlem26  46413  wallispilem3  46454  stirlinglem6  46466  stirlinglem11  46471  dirkertrigeqlem1  46485  sqwvfourb  46616  fourierswlem  46617  addmodne  47733  fmtno5lem1  47942  fmtno5lem4  47945  257prm  47950  fmtnoprmfac1lem  47953  fmtnofac1  47959  127prm  47988  m11nprm  47990  lighneallem2  47995  proththd  48003  opoeALTV  48072  1oddALTV  48079  nnsum3primes4  48177  nnsum3primesgbe  48181  nnsum4primesodd  48185  nnsum4primesoddALTV  48186  bgoldbtbndlem1  48194  grtriclwlk3  48334  cycl3grtrilem  48335  gpgprismgr4cycllem10  48493  oddinmgm  48564  fldivexpfllog2  48954  blen2  48974  ackval1  49070  ackval0012  49078