Theorem 1p1e2 11756

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

Syntax hints:   = wceq 1533  (class class class)co 7150  1c1 10532   + caddc 10534  2c2 11686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-2 11694

This theorem is referenced by:  2m1e1  11757  1p2e3  11774  add1p1  11882  sub1m1  11883  nn0n0n1ge2  11956  3halfnz  12055  10p10e20  12187  5t4e20  12194  6t4e24  12198  7t3e21  12202  8t3e24  12208  9t3e27  12215  fz12pr  12958  fz0to3un2pr  13003  fzo13pr  13115  fzo1to4tp  13119  fldiv4p1lem1div2  13199  m1modge3gt1  13280  fac2  13633  hash2  13760  hashprlei  13820  ccat2s1len  13971  ccat2s1lenOLD  13972  ccat2s1p2  13980  ccat2s1p2OLD  13982  s2len  14245  repsw2  14306  swrd2lsw  14308  2swrd2eqwrdeq  14309  nn0o1gt2  15726  3lcm2e6woprm  15953  ge2nprmge4  16039  2exp8  16417  2exp16  16418  prmlem0  16433  prmlem2  16447  37prm  16448  43prm  16449  83prm  16450  317prm  16453  631prm  16454  1259lem1  16458  1259lem2  16459  1259lem4  16461  1259lem5  16462  2503lem1  16464  2503lem2  16465  2503lem3  16466  2503prm  16467  4001lem2  16469  4001lem3  16470  4001lem4  16471  m2detleiblem2  21231  logbleb  25355  logblt  25356  log2ublem3  25520  log2ub  25521  1sgm2ppw  25770  2sqb  26002  2sq2  26003  rplogsumlem2  26055  tgldimor  26282  1loopgrvd2  27279  2wlklem  27443  pthdlem1  27541  pthdlem2  27543  wwlksnextwrd  27669  wwlksnextproplem3  27684  2wlkdlem5  27702  2wlkdlem10  27708  rusgrnumwwlkl1  27741  clwlkclwwlklem2a4  27769  clwlkclwwlklem2a  27770  clwwlkext2edg  27829  wwlksext2clwwlk  27830  clwlknf1oclwwlknlem1  27854  3wlkdlem5  27936  3wlkdlem10  27942  upgr3v3e3cycl  27953  upgr4cycl4dv4e  27958  konigsberglem1  28025  konigsberglem2  28026  konigsberglem3  28027  numclwlk2lem2f  28150  ex-exp  28223  1nei  30466  psgnfzto1st  30742  cyc3fv2  30775  archirngz  30813  archiabllem2c  30819  lmat22e12  31079  lmat22e21  31080  lmat22e22  31081  madjusmdetlem4  31090  fiblem  31651  fibp1  31654  fib2  31655  fib3  31656  ballotlem2  31741  ballotlemfc0  31745  ballotlemfcc  31746  signstfveq0  31842  chtvalz  31895  hgt750lem  31917  hgt750lem2  31918  subfacp1lem5  32426  dnibndlem13  33824  knoppndvlem12  33857  sn-0ne2  39229  fltnltalem  39267  rabren3dioph  39405  pellfundgt1  39473  areaquad  39816  trclfvdecomr  40066  xralrple2  41615  sumnnodd  41904  itgsin0pilem1  42228  itgsinexp  42233  stoweidlem14  42293  stoweidlem26  42305  wallispilem3  42346  stirlinglem6  42358  stirlinglem11  42363  dirkertrigeqlem1  42377  sqwvfourb  42508  fourierswlem  42509  fmtno5lem1  43709  fmtno5lem4  43712  257prm  43717  fmtnoprmfac1lem  43720  fmtnofac1  43726  127prm  43757  2exp11  43759  m11nprm  43760  lighneallem2  43765  proththd  43773  opoeALTV  43842  1oddALTV  43849  nnsum3primes4  43947  nnsum3primesgbe  43951  nnsum4primesodd  43955  nnsum4primesoddALTV  43956  bgoldbtbndlem1  43964  oddinmgm  44076  fldivexpfllog2  44619  blen2  44639