Theorem 1p1e2 11765

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

Syntax hints:   = wceq 1536  (class class class)co 7159  1c1 10541   + caddc 10543  2c2 11695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-2 11703

This theorem is referenced by:  2m1e1  11766  1p2e3  11783  add1p1  11891  sub1m1  11892  nn0n0n1ge2  11965  3halfnz  12064  10p10e20  12196  5t4e20  12203  6t4e24  12207  7t3e21  12211  8t3e24  12217  9t3e27  12224  fz12pr  12967  fz0to3un2pr  13012  fzo13pr  13124  fzo1to4tp  13128  fldiv4p1lem1div2  13208  m1modge3gt1  13289  fac2  13642  hash2  13769  hashprlei  13829  ccat2s1len  13980  ccat2s1lenOLD  13981  ccat2s1p2  13989  ccat2s1p2OLD  13991  s2len  14254  repsw2  14315  swrd2lsw  14317  2swrd2eqwrdeq  14318  nn0o1gt2  15735  3lcm2e6woprm  15962  ge2nprmge4  16048  2exp8  16426  2exp16  16427  prmlem0  16442  prmlem2  16456  37prm  16457  43prm  16458  83prm  16459  317prm  16462  631prm  16463  1259lem1  16467  1259lem2  16468  1259lem4  16470  1259lem5  16471  2503lem1  16473  2503lem2  16474  2503lem3  16475  2503prm  16476  4001lem2  16478  4001lem3  16479  4001lem4  16480  m2detleiblem2  21240  logbleb  25364  logblt  25365  log2ublem3  25529  log2ub  25530  1sgm2ppw  25779  2sqb  26011  2sq2  26012  rplogsumlem2  26064  tgldimor  26291  1loopgrvd2  27288  2wlklem  27452  pthdlem1  27550  pthdlem2  27552  wwlksnextwrd  27678  wwlksnextproplem3  27693  2wlkdlem5  27711  2wlkdlem10  27717  rusgrnumwwlkl1  27750  clwlkclwwlklem2a4  27778  clwlkclwwlklem2a  27779  clwwlkext2edg  27838  wwlksext2clwwlk  27839  clwlknf1oclwwlknlem1  27863  3wlkdlem5  27945  3wlkdlem10  27951  upgr3v3e3cycl  27962  upgr4cycl4dv4e  27967  konigsberglem1  28034  konigsberglem2  28035  konigsberglem3  28036  numclwlk2lem2f  28159  ex-exp  28232  1nei  30475  psgnfzto1st  30751  cyc3fv2  30784  archirngz  30822  archiabllem2c  30828  lmat22e12  31088  lmat22e21  31089  lmat22e22  31090  madjusmdetlem4  31099  fiblem  31660  fibp1  31663  fib2  31664  fib3  31665  ballotlem2  31750  ballotlemfc0  31754  ballotlemfcc  31755  signstfveq0  31851  chtvalz  31904  hgt750lem  31926  hgt750lem2  31927  subfacp1lem5  32435  dnibndlem13  33833  knoppndvlem12  33866  sn-0ne2  39242  fltnltalem  39280  rabren3dioph  39418  pellfundgt1  39486  areaquad  39829  trclfvdecomr  40079  xralrple2  41628  sumnnodd  41917  itgsin0pilem1  42241  itgsinexp  42246  stoweidlem14  42306  stoweidlem26  42318  wallispilem3  42359  stirlinglem6  42371  stirlinglem11  42376  dirkertrigeqlem1  42390  sqwvfourb  42521  fourierswlem  42522  fmtno5lem1  43722  fmtno5lem4  43725  257prm  43730  fmtnoprmfac1lem  43733  fmtnofac1  43739  127prm  43770  2exp11  43772  m11nprm  43773  lighneallem2  43778  proththd  43786  opoeALTV  43855  1oddALTV  43862  nnsum3primes4  43960  nnsum3primesgbe  43964  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  bgoldbtbndlem1  43977  oddinmgm  44089  fldivexpfllog2  44632  blen2  44652