Theorem 1p1e2 12269

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

Syntax hints:   = wceq 1542  (class class class)co 7360  1c1 11031   + caddc 11033  2c2 12204

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 12212

This theorem is referenced by:  2m1e1  12270  1p2e3  12287  add1p1  12396  sub1m1  12397  nn0n0n1ge2  12473  3halfnz  12575  10p10e20  12706  5t4e20  12713  6t4e24  12717  7t3e21  12721  8t3e24  12727  9t3e27  12734  fz12pr  13501  fz0to3un2pr  13549  fzo13pr  13669  fzo1to4tp  13674  fldiv4p1lem1div2  13759  m1modge3gt1  13845  fac2  14206  hash2  14332  hashprlei  14395  ccat2s1len  14551  ccat2s1p2  14558  s2len  14816  repsw2  14877  swrd2lsw  14879  2swrd2eqwrdeq  14880  nn0o1gt2  16312  3lcm2e6woprm  16546  ge2nprmge4  16632  2exp8  17020  2exp11  17021  2exp16  17022  prmlem0  17037  prmlem2  17051  37prm  17052  43prm  17053  83prm  17054  317prm  17057  631prm  17058  1259lem1  17062  1259lem2  17063  1259lem4  17065  1259lem5  17066  2503lem1  17068  2503lem2  17069  2503lem3  17070  2503prm  17071  4001lem2  17073  4001lem3  17074  4001lem4  17075  m2detleiblem2  22576  logbleb  26753  logblt  26754  log2ublem3  26918  log2ub  26919  1sgm2ppw  27171  2sqb  27403  2sq2  27404  rplogsumlem2  27456  tgldimor  28578  1loopgrvd2  29581  2wlklem  29743  pthdlem1  29843  pthdlem2  29845  wwlksnextwrd  29974  wwlksnextproplem3  29988  2wlkdlem5  30006  2wlkdlem10  30012  rusgrnumwwlkl1  30048  clwlkclwwlklem2a4  30076  clwlkclwwlklem2a  30077  clwwlkext2edg  30135  wwlksext2clwwlk  30136  clwlknf1oclwwlknlem1  30160  3wlkdlem5  30242  3wlkdlem10  30248  upgr3v3e3cycl  30259  upgr4cycl4dv4e  30264  konigsberglem1  30331  konigsberglem2  30332  konigsberglem3  30333  numclwlk2lem2f  30456  ex-exp  30529  1nei  32818  psgnfzto1st  33189  cyc3fv2  33222  archirngz  33273  archiabllem2c  33279  cos9thpiminplylem1  33941  lmat22e12  33978  lmat22e21  33979  lmat22e22  33980  madjusmdetlem4  33989  fiblem  34557  fibp1  34560  fib2  34561  fib3  34562  ballotlem2  34648  ballotlemfc0  34652  ballotlemfcc  34653  signstfveq0  34736  chtvalz  34788  hgt750lem  34810  hgt750lem2  34811  subfacp1lem5  35380  dnibndlem13  36692  knoppndvlem12  36725  420gcd8e4  42328  3exp7  42375  3lexlogpow5ineq1  42376  aks4d1p1  42398  2np3bcnp1  42466  sn-0ne2  42728  flt0  42947  fltnltalem  42972  rabren3dioph  43124  pellfundgt1  43192  areaquad  43525  resqrtvalex  43953  imsqrtvalex  43954  trclfvdecomr  44036  xralrple2  45666  sumnnodd  45943  itgsin0pilem1  46261  itgsinexp  46266  stoweidlem14  46325  stoweidlem26  46337  wallispilem3  46378  stirlinglem6  46390  stirlinglem11  46395  dirkertrigeqlem1  46409  sqwvfourb  46540  fourierswlem  46541  addmodne  47657  fmtno5lem1  47866  fmtno5lem4  47869  257prm  47874  fmtnoprmfac1lem  47877  fmtnofac1  47883  127prm  47912  m11nprm  47914  lighneallem2  47919  proththd  47927  opoeALTV  47996  1oddALTV  48003  nnsum3primes4  48101  nnsum3primesgbe  48105  nnsum4primesodd  48109  nnsum4primesoddALTV  48110  bgoldbtbndlem1  48118  grtriclwlk3  48258  cycl3grtrilem  48259  gpgprismgr4cycllem10  48417  oddinmgm  48488  fldivexpfllog2  48878  blen2  48898  ackval1  48994  ackval0012  49002