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  27784  1loopgrvd2  28791  2wlklem  28955  pthdlem1  29054  pthdlem2  29056  wwlksnextwrd  29182  wwlksnextproplem3  29196  2wlkdlem5  29214  2wlkdlem10  29220  rusgrnumwwlkl1  29253  clwlkclwwlklem2a4  29281  clwlkclwwlklem2a  29282  clwwlkext2edg  29340  wwlksext2clwwlk  29341  clwlknf1oclwwlknlem1  29365  3wlkdlem5  29447  3wlkdlem10  29453  upgr3v3e3cycl  29464  upgr4cycl4dv4e  29469  konigsberglem1  29536  konigsberglem2  29537  konigsberglem3  29538  numclwlk2lem2f  29661  ex-exp  29734  1nei  31992  psgnfzto1st  32295  cyc3fv2  32328  archirngz  32366  archiabllem2c  32372  lmat22e12  32830  lmat22e21  32831  lmat22e22  32832  madjusmdetlem4  32841  fiblem  33428  fibp1  33431  fib2  33432  fib3  33433  ballotlem2  33518  ballotlemfc0  33522  ballotlemfcc  33523  signstfveq0  33619  chtvalz  33672  hgt750lem  33694  hgt750lem2  33695  subfacp1lem5  34206  dnibndlem13  35414  knoppndvlem12  35447  420gcd8e4  40919  3exp7  40966  3lexlogpow5ineq1  40967  aks4d1p1  40989  2np3bcnp1  41008  sn-0ne2  41327  flt0  41427  fltnltalem  41452  rabren3dioph  41601  pellfundgt1  41669  areaquad  42013  resqrtvalex  42444  imsqrtvalex  42445  trclfvdecomr  42527  xralrple2  44112  sumnnodd  44394  itgsin0pilem1  44714  itgsinexp  44719  stoweidlem14  44778  stoweidlem26  44790  wallispilem3  44831  stirlinglem6  44843  stirlinglem11  44848  dirkertrigeqlem1  44862  sqwvfourb  44993  fourierswlem  44994  fmtno5lem1  46269  fmtno5lem4  46272  257prm  46277  fmtnoprmfac1lem  46280  fmtnofac1  46286  127prm  46315  m11nprm  46317  lighneallem2  46322  proththd  46330  opoeALTV  46399  1oddALTV  46406  nnsum3primes4  46504  nnsum3primesgbe  46508  nnsum4primesodd  46512  nnsum4primesoddALTV  46513  bgoldbtbndlem1  46521  oddinmgm  46633  fldivexpfllog2  47299  blen2  47319  ackval1  47415  ackval0012  47423