Theorem 1p1e2 12028

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

Syntax hints:   = wceq 1539  (class class class)co 7255  1c1 10803   + caddc 10805  2c2 11958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-2 11966

This theorem is referenced by:  2m1e1  12029  1p2e3  12046  add1p1  12154  sub1m1  12155  nn0n0n1ge2  12230  3halfnz  12329  10p10e20  12461  5t4e20  12468  6t4e24  12472  7t3e21  12476  8t3e24  12482  9t3e27  12489  fz12pr  13242  fz0to3un2pr  13287  fzo13pr  13399  fzo1to4tp  13403  fldiv4p1lem1div2  13483  m1modge3gt1  13566  fac2  13921  hash2  14048  hashprlei  14110  ccat2s1len  14256  ccat2s1lenOLD  14257  ccat2s1p2  14265  ccat2s1p2OLD  14267  s2len  14530  repsw2  14591  swrd2lsw  14593  2swrd2eqwrdeq  14594  nn0o1gt2  16018  3lcm2e6woprm  16248  ge2nprmge4  16334  2exp8  16718  2exp11  16719  2exp16  16720  prmlem0  16735  prmlem2  16749  37prm  16750  43prm  16751  83prm  16752  317prm  16755  631prm  16756  1259lem1  16760  1259lem2  16761  1259lem4  16763  1259lem5  16764  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem2  16771  4001lem3  16772  4001lem4  16773  m2detleiblem2  21685  logbleb  25838  logblt  25839  log2ublem3  26003  log2ub  26004  1sgm2ppw  26253  2sqb  26485  2sq2  26486  rplogsumlem2  26538  tgldimor  26767  1loopgrvd2  27773  2wlklem  27937  pthdlem1  28035  pthdlem2  28037  wwlksnextwrd  28163  wwlksnextproplem3  28177  2wlkdlem5  28195  2wlkdlem10  28201  rusgrnumwwlkl1  28234  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwwlkext2edg  28321  wwlksext2clwwlk  28322  clwlknf1oclwwlknlem1  28346  3wlkdlem5  28428  3wlkdlem10  28434  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  numclwlk2lem2f  28642  ex-exp  28715  1nei  30973  psgnfzto1st  31274  cyc3fv2  31307  archirngz  31345  archiabllem2c  31351  lmat22e12  31671  lmat22e21  31672  lmat22e22  31673  madjusmdetlem4  31682  fiblem  32265  fibp1  32268  fib2  32269  fib3  32270  ballotlem2  32355  ballotlemfc0  32359  ballotlemfcc  32360  signstfveq0  32456  chtvalz  32509  hgt750lem  32531  hgt750lem2  32532  subfacp1lem5  33046  dnibndlem13  34597  knoppndvlem12  34630  420gcd8e4  39942  3exp7  39989  3lexlogpow5ineq1  39990  aks4d1p1  40012  2np3bcnp1  40028  sn-0ne2  40310  flt0  40390  fltnltalem  40415  rabren3dioph  40553  pellfundgt1  40621  areaquad  40963  resqrtvalex  41142  imsqrtvalex  41143  trclfvdecomr  41225  xralrple2  42783  sumnnodd  43061  itgsin0pilem1  43381  itgsinexp  43386  stoweidlem14  43445  stoweidlem26  43457  wallispilem3  43498  stirlinglem6  43510  stirlinglem11  43515  dirkertrigeqlem1  43529  sqwvfourb  43660  fourierswlem  43661  fmtno5lem1  44893  fmtno5lem4  44896  257prm  44901  fmtnoprmfac1lem  44904  fmtnofac1  44910  127prm  44939  m11nprm  44941  lighneallem2  44946  proththd  44954  opoeALTV  45023  1oddALTV  45030  nnsum3primes4  45128  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  bgoldbtbndlem1  45145  oddinmgm  45257  fldivexpfllog2  45799  blen2  45819  ackval1  45915  ackval0012  45923