Theorem 1p1e2 11134

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 11079	. 2 |- 2 = ( 1 + 1 )
2	1	eqcomi 2631	1 |- ( 1 + 1 ) = 2

Syntax hints:   = wceq 1483  (class class class)co 6650   1c1 9937   + caddc 9939   2c2 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-2 11079

This theorem is referenced by:  2m1e1  11135  add1p1  11283  sub1m1  11284  nn0n0n1ge2  11358  3halfnz  11456  10p10e20  11628  10p10e20OLD  11629  5t4e20  11637  5t4e20OLD  11638  6t4e24  11643  7t3e21  11649  8t3e24  11655  9t3e27  11664  fz0to3un2pr  12441  fzo13pr  12552  fzo1to4tp  12556  fldiv4p1lem1div2  12636  m1modge3gt1  12717  fac2  13066  hash2  13193  hashprlei  13250  ccat2s1len  13400  ccat2s1p2  13406  s2len  13634  repsw2  13693  swrd2lsw  13695  2swrd2eqwrdeq  13696  nn0o1gt2  15097  3lcm2e6woprm  15328  2exp8  15796  2exp16  15797  prmlem0  15812  prmlem2  15827  37prm  15828  43prm  15829  83prm  15830  317prm  15833  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem4  15841  1259lem5  15842  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem2  15849  4001lem3  15850  4001lem4  15851  m2detleiblem2  20434  iblcnlem1  23554  logbleb  24521  logblt  24522  log2ublem3  24675  log2ub  24676  1sgm2ppw  24925  2sqb  25157  rplogsumlem2  25174  tgldimor  25397  1loopgrvd2  26399  2wlklem  26563  pthdlem1  26662  pthdlem2  26664  wwlksnextwrd  26792  wwlksnextproplem3  26806  2wlkdlem5  26825  2wlkdlem10  26831  rusgrnumwwlkl1  26863  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwwlksext2edg  26923  wwlksext2clwwlk  26924  3wlkdlem5  27023  3wlkdlem10  27029  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  numclwlk1lem2fo  27228  numclwlk2lem2f  27236  ex-exp  27307  archirngz  29743  archiabllem2c  29749  psgnfzto1st  29855  lmat22e12  29885  lmat22e21  29886  lmat22e22  29887  madjusmdetlem4  29896  fiblem  30460  fibp1  30463  fib2  30464  fib3  30465  ballotlem2  30550  ballotlemfc0  30554  ballotlemfcc  30555  signstfveq0  30654  chtvalz  30707  hgt750lem  30729  hgt750lem2  30730  subfacp1lem5  31166  dnibndlem13  32480  knoppndvlem12  32514  rabren3dioph  37379  pellfundgt1  37447  areaquad  37802  trclfvdecomr  38020  xralrple2  39570  sumnnodd  39862  itgsin0pilem1  40165  itgsinexp  40170  stoweidlem14  40231  stoweidlem26  40243  wallispilem3  40284  stirlinglem6  40296  stirlinglem11  40301  dirkertrigeqlem1  40315  sqwvfourb  40446  fourierswlem  40447  fmtno5lem1  41465  fmtno5lem4  41468  257prm  41473  fmtnoprmfac1lem  41476  fmtnofac1  41482  127prm  41515  2exp11  41517  m11nprm  41518  lighneallem2  41523  proththd  41531  opoeALTV  41594  1oddALTV  41601  nnsum3primes4  41676  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  bgoldbtbndlem1  41693  oddinmgm  41815  fldivexpfllog2  42359  blen2  42379