Theorem 1p1e2 12245

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

Syntax hints:   = wceq 1541  (class class class)co 7346  1c1 11007   + caddc 11009  2c2 12180

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 2121  ax-ext 2703

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

This theorem is referenced by:  2m1e1  12246  1p2e3  12263  add1p1  12372  sub1m1  12373  nn0n0n1ge2  12449  3halfnz  12552  10p10e20  12683  5t4e20  12690  6t4e24  12694  7t3e21  12698  8t3e24  12704  9t3e27  12711  fz12pr  13481  fz0to3un2pr  13529  fzo13pr  13649  fzo1to4tp  13654  fldiv4p1lem1div2  13739  m1modge3gt1  13825  fac2  14186  hash2  14312  hashprlei  14375  ccat2s1len  14531  ccat2s1p2  14538  s2len  14796  repsw2  14857  swrd2lsw  14859  2swrd2eqwrdeq  14860  nn0o1gt2  16292  3lcm2e6woprm  16526  ge2nprmge4  16612  2exp8  17000  2exp11  17001  2exp16  17002  prmlem0  17017  prmlem2  17031  37prm  17032  43prm  17033  83prm  17034  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem2  17053  4001lem3  17054  4001lem4  17055  m2detleiblem2  22543  logbleb  26720  logblt  26721  log2ublem3  26885  log2ub  26886  1sgm2ppw  27138  2sqb  27370  2sq2  27371  rplogsumlem2  27423  tgldimor  28480  1loopgrvd2  29482  2wlklem  29644  pthdlem1  29744  pthdlem2  29746  wwlksnextwrd  29875  wwlksnextproplem3  29889  2wlkdlem5  29907  2wlkdlem10  29913  rusgrnumwwlkl1  29949  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  clwwlkext2edg  30036  wwlksext2clwwlk  30037  clwlknf1oclwwlknlem1  30061  3wlkdlem5  30143  3wlkdlem10  30149  upgr3v3e3cycl  30160  upgr4cycl4dv4e  30165  konigsberglem1  30232  konigsberglem2  30233  konigsberglem3  30234  numclwlk2lem2f  30357  ex-exp  30430  1nei  32720  psgnfzto1st  33074  cyc3fv2  33107  archirngz  33158  archiabllem2c  33164  cos9thpiminplylem1  33795  lmat22e12  33832  lmat22e21  33833  lmat22e22  33834  madjusmdetlem4  33843  fiblem  34411  fibp1  34414  fib2  34415  fib3  34416  ballotlem2  34502  ballotlemfc0  34506  ballotlemfcc  34507  signstfveq0  34590  chtvalz  34642  hgt750lem  34664  hgt750lem2  34665  subfacp1lem5  35228  dnibndlem13  36534  knoppndvlem12  36567  420gcd8e4  42109  3exp7  42156  3lexlogpow5ineq1  42157  aks4d1p1  42179  2np3bcnp1  42247  sn-0ne2  42509  flt0  42740  fltnltalem  42765  rabren3dioph  42918  pellfundgt1  42986  areaquad  43319  resqrtvalex  43748  imsqrtvalex  43749  trclfvdecomr  43831  xralrple2  45463  sumnnodd  45740  itgsin0pilem1  46058  itgsinexp  46063  stoweidlem14  46122  stoweidlem26  46134  wallispilem3  46175  stirlinglem6  46187  stirlinglem11  46192  dirkertrigeqlem1  46206  sqwvfourb  46337  fourierswlem  46338  addmodne  47454  fmtno5lem1  47663  fmtno5lem4  47666  257prm  47671  fmtnoprmfac1lem  47674  fmtnofac1  47680  127prm  47709  m11nprm  47711  lighneallem2  47716  proththd  47724  opoeALTV  47793  1oddALTV  47800  nnsum3primes4  47898  nnsum3primesgbe  47902  nnsum4primesodd  47906  nnsum4primesoddALTV  47907  bgoldbtbndlem1  47915  grtriclwlk3  48055  cycl3grtrilem  48056  gpgprismgr4cycllem10  48214  oddinmgm  48285  fldivexpfllog2  48676  blen2  48696  ackval1  48792  ackval0012  48800