Theorem 1p1e2 11599

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

Syntax hints:   = wceq 1520  (class class class)co 7007  1c1 10373   + caddc 10375  2c2 11529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786  df-2 11537

This theorem is referenced by:  2m1e1  11600  1p2e3  11617  add1p1  11725  sub1m1  11726  nn0n0n1ge2  11799  3halfnz  11899  10p10e20  12032  5t4e20  12039  6t4e24  12043  7t3e21  12047  8t3e24  12053  9t3e27  12060  fz12pr  12803  fz0to3un2pr  12848  fzo13pr  12959  fzo1to4tp  12963  fldiv4p1lem1div2  13043  m1modge3gt1  13124  fac2  13477  hash2  13602  hashprlei  13660  ccat2s1len  13809  ccat2s1p2  13816  s2len  14075  repsw2  14136  swrd2lsw  14138  2swrd2eqwrdeq  14139  nn0o1gt2  15553  3lcm2e6woprm  15776  ge2nprmge4  15862  2exp8  16240  2exp16  16241  prmlem0  16256  prmlem2  16270  37prm  16271  43prm  16272  83prm  16273  317prm  16276  631prm  16277  1259lem1  16281  1259lem2  16282  1259lem4  16284  1259lem5  16285  2503lem1  16287  2503lem2  16288  2503lem3  16289  2503prm  16290  4001lem2  16292  4001lem3  16293  4001lem4  16294  m2detleiblem2  20909  logbleb  25030  logblt  25031  log2ublem3  25196  log2ub  25197  1sgm2ppw  25446  2sqb  25678  2sq2  25679  rplogsumlem2  25731  tgldimor  25958  1loopgrvd2  26956  2wlklem  27119  pthdlem1  27222  pthdlem2  27224  wwlksnextwrd  27350  wwlksnextproplem3  27365  2wlkdlem5  27383  2wlkdlem10  27389  rusgrnumwwlkl1  27422  clwlkclwwlklem2a4  27450  clwlkclwwlklem2a  27451  clwwlkext2edg  27510  wwlksext2clwwlk  27511  clwlknf1oclwwlknlem1  27535  3wlkdlem5  27617  3wlkdlem10  27623  upgr3v3e3cycl  27634  upgr4cycl4dv4e  27639  konigsberglem1  27709  konigsberglem2  27710  konigsberglem3  27711  numclwlk2lem2f  27836  ex-exp  27909  1nei  30133  cyc3fv2  30380  archirngz  30414  archiabllem2c  30420  psgnfzto1st  30625  lmat22e12  30655  lmat22e21  30656  lmat22e22  30657  madjusmdetlem4  30666  fiblem  31229  fibp1  31232  fib2  31233  fib3  31234  ballotlem2  31319  ballotlemfc0  31323  ballotlemfcc  31324  signstfveq0  31420  chtvalz  31473  hgt750lem  31495  hgt750lem2  31496  subfacp1lem5  31995  dnibndlem13  33382  knoppndvlem12  33415  fltnltalem  38721  rabren3dioph  38848  pellfundgt1  38916  areaquad  39259  trclfvdecomr  39509  xralrple2  41116  sumnnodd  41407  itgsin0pilem1  41730  itgsinexp  41735  stoweidlem14  41795  stoweidlem26  41807  wallispilem3  41848  stirlinglem6  41860  stirlinglem11  41865  dirkertrigeqlem1  41879  sqwvfourb  42010  fourierswlem  42011  fmtno5lem1  43151  fmtno5lem4  43154  257prm  43159  fmtnoprmfac1lem  43162  fmtnofac1  43168  127prm  43199  2exp11  43201  m11nprm  43202  lighneallem2  43207  proththd  43215  opoeALTV  43284  1oddALTV  43291  nnsum3primes4  43389  nnsum3primesgbe  43393  nnsum4primesodd  43397  nnsum4primesoddALTV  43398  bgoldbtbndlem1  43406  oddinmgm  43518  fldivexpfllog2  44060  blen2  44080