Theorem 1p1e2 12263

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

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   + caddc 11027  2c2 12198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-2 12206

This theorem is referenced by:  2m1e1  12264  1p2e3  12281  add1p1  12390  sub1m1  12391  nn0n0n1ge2  12467  3halfnz  12569  10p10e20  12700  5t4e20  12707  6t4e24  12711  7t3e21  12715  8t3e24  12721  9t3e27  12728  fz12pr  13495  fz0to3un2pr  13543  fzo13pr  13663  fzo1to4tp  13668  fldiv4p1lem1div2  13753  m1modge3gt1  13839  fac2  14200  hash2  14326  hashprlei  14389  ccat2s1len  14545  ccat2s1p2  14552  s2len  14810  repsw2  14871  swrd2lsw  14873  2swrd2eqwrdeq  14874  nn0o1gt2  16306  3lcm2e6woprm  16540  ge2nprmge4  16626  2exp8  17014  2exp11  17015  2exp16  17016  prmlem0  17031  prmlem2  17045  37prm  17046  43prm  17047  83prm  17048  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem4  17059  1259lem5  17060  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem2  17067  4001lem3  17068  4001lem4  17069  m2detleiblem2  22570  logbleb  26747  logblt  26748  log2ublem3  26912  log2ub  26913  1sgm2ppw  27165  2sqb  27397  2sq2  27398  rplogsumlem2  27450  tgldimor  28523  1loopgrvd2  29526  2wlklem  29688  pthdlem1  29788  pthdlem2  29790  wwlksnextwrd  29919  wwlksnextproplem3  29933  2wlkdlem5  29951  2wlkdlem10  29957  rusgrnumwwlkl1  29993  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  clwwlkext2edg  30080  wwlksext2clwwlk  30081  clwlknf1oclwwlknlem1  30105  3wlkdlem5  30187  3wlkdlem10  30193  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  konigsberglem1  30276  konigsberglem2  30277  konigsberglem3  30278  numclwlk2lem2f  30401  ex-exp  30474  1nei  32765  psgnfzto1st  33136  cyc3fv2  33169  archirngz  33220  archiabllem2c  33226  cos9thpiminplylem1  33888  lmat22e12  33925  lmat22e21  33926  lmat22e22  33927  madjusmdetlem4  33936  fiblem  34504  fibp1  34507  fib2  34508  fib3  34509  ballotlem2  34595  ballotlemfc0  34599  ballotlemfcc  34600  signstfveq0  34683  chtvalz  34735  hgt750lem  34757  hgt750lem2  34758  subfacp1lem5  35327  dnibndlem13  36633  knoppndvlem12  36666  420gcd8e4  42199  3exp7  42246  3lexlogpow5ineq1  42247  aks4d1p1  42269  2np3bcnp1  42337  sn-0ne2  42603  flt0  42822  fltnltalem  42847  rabren3dioph  42999  pellfundgt1  43067  areaquad  43400  resqrtvalex  43828  imsqrtvalex  43829  trclfvdecomr  43911  xralrple2  45541  sumnnodd  45818  itgsin0pilem1  46136  itgsinexp  46141  stoweidlem14  46200  stoweidlem26  46212  wallispilem3  46253  stirlinglem6  46265  stirlinglem11  46270  dirkertrigeqlem1  46284  sqwvfourb  46415  fourierswlem  46416  addmodne  47532  fmtno5lem1  47741  fmtno5lem4  47744  257prm  47749  fmtnoprmfac1lem  47752  fmtnofac1  47758  127prm  47787  m11nprm  47789  lighneallem2  47794  proththd  47802  opoeALTV  47871  1oddALTV  47878  nnsum3primes4  47976  nnsum3primesgbe  47980  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  bgoldbtbndlem1  47993  grtriclwlk3  48133  cycl3grtrilem  48134  gpgprismgr4cycllem10  48292  oddinmgm  48363  fldivexpfllog2  48753  blen2  48773  ackval1  48869  ackval0012  48877