Theorem 1p1e2 12337

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

Syntax hints:   = wceq 1542  (class class class)co 7409  1c1 11111   + caddc 11113  2c2 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-2 12275

This theorem is referenced by:  2m1e1  12338  1p2e3  12355  add1p1  12463  sub1m1  12464  nn0n0n1ge2  12539  3halfnz  12641  10p10e20  12772  5t4e20  12779  6t4e24  12783  7t3e21  12787  8t3e24  12793  9t3e27  12800  fz12pr  13558  fz0to3un2pr  13603  fzo13pr  13716  fzo1to4tp  13720  fldiv4p1lem1div2  13800  m1modge3gt1  13883  fac2  14239  hash2  14365  hashprlei  14429  ccat2s1len  14573  ccat2s1p2  14580  s2len  14840  repsw2  14901  swrd2lsw  14903  2swrd2eqwrdeq  14904  nn0o1gt2  16324  3lcm2e6woprm  16552  ge2nprmge4  16638  2exp8  17022  2exp11  17023  2exp16  17024  prmlem0  17039  prmlem2  17053  37prm  17054  43prm  17055  83prm  17056  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem4  17067  1259lem5  17068  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem2  17075  4001lem3  17076  4001lem4  17077  m2detleiblem2  22130  logbleb  26288  logblt  26289  log2ublem3  26453  log2ub  26454  1sgm2ppw  26703  2sqb  26935  2sq2  26936  rplogsumlem2  26988  tgldimor  27753  1loopgrvd2  28760  2wlklem  28924  pthdlem1  29023  pthdlem2  29025  wwlksnextwrd  29151  wwlksnextproplem3  29165  2wlkdlem5  29183  2wlkdlem10  29189  rusgrnumwwlkl1  29222  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwwlkext2edg  29309  wwlksext2clwwlk  29310  clwlknf1oclwwlknlem1  29334  3wlkdlem5  29416  3wlkdlem10  29422  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  konigsberglem1  29505  konigsberglem2  29506  konigsberglem3  29507  numclwlk2lem2f  29630  ex-exp  29703  1nei  31961  psgnfzto1st  32264  cyc3fv2  32297  archirngz  32335  archiabllem2c  32341  lmat22e12  32799  lmat22e21  32800  lmat22e22  32801  madjusmdetlem4  32810  fiblem  33397  fibp1  33400  fib2  33401  fib3  33402  ballotlem2  33487  ballotlemfc0  33491  ballotlemfcc  33492  signstfveq0  33588  chtvalz  33641  hgt750lem  33663  hgt750lem2  33664  subfacp1lem5  34175  dnibndlem13  35366  knoppndvlem12  35399  420gcd8e4  40871  3exp7  40918  3lexlogpow5ineq1  40919  aks4d1p1  40941  2np3bcnp1  40960  sn-0ne2  41279  flt0  41379  fltnltalem  41404  rabren3dioph  41553  pellfundgt1  41621  areaquad  41965  resqrtvalex  42396  imsqrtvalex  42397  trclfvdecomr  42479  xralrple2  44064  sumnnodd  44346  itgsin0pilem1  44666  itgsinexp  44671  stoweidlem14  44730  stoweidlem26  44742  wallispilem3  44783  stirlinglem6  44795  stirlinglem11  44800  dirkertrigeqlem1  44814  sqwvfourb  44945  fourierswlem  44946  fmtno5lem1  46221  fmtno5lem4  46224  257prm  46229  fmtnoprmfac1lem  46232  fmtnofac1  46238  127prm  46267  m11nprm  46269  lighneallem2  46274  proththd  46282  opoeALTV  46351  1oddALTV  46358  nnsum3primes4  46456  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  bgoldbtbndlem1  46473  oddinmgm  46585  fldivexpfllog2  47251  blen2  47271  ackval1  47367  ackval0012  47375