Theorem 1p1e2 12363

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

Syntax hints:   = wceq 1540  (class class class)co 7403  1c1 11128   + caddc 11130  2c2 12293

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 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-2 12301

This theorem is referenced by:  2m1e1  12364  1p2e3  12381  add1p1  12490  sub1m1  12491  nn0n0n1ge2  12567  3halfnz  12670  10p10e20  12801  5t4e20  12808  6t4e24  12812  7t3e21  12816  8t3e24  12822  9t3e27  12829  fz12pr  13596  fz0to3un2pr  13644  fzo13pr  13763  fzo1to4tp  13768  fldiv4p1lem1div2  13850  m1modge3gt1  13934  fac2  14295  hash2  14421  hashprlei  14484  ccat2s1len  14639  ccat2s1p2  14646  s2len  14906  repsw2  14967  swrd2lsw  14969  2swrd2eqwrdeq  14970  nn0o1gt2  16398  3lcm2e6woprm  16632  ge2nprmge4  16718  2exp8  17106  2exp11  17107  2exp16  17108  prmlem0  17123  prmlem2  17137  37prm  17138  43prm  17139  83prm  17140  317prm  17143  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem4  17151  1259lem5  17152  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem2  17159  4001lem3  17160  4001lem4  17161  m2detleiblem2  22564  logbleb  26743  logblt  26744  log2ublem3  26908  log2ub  26909  1sgm2ppw  27161  2sqb  27393  2sq2  27394  rplogsumlem2  27446  tgldimor  28427  1loopgrvd2  29429  2wlklem  29593  pthdlem1  29694  pthdlem2  29696  wwlksnextwrd  29825  wwlksnextproplem3  29839  2wlkdlem5  29857  2wlkdlem10  29863  rusgrnumwwlkl1  29896  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwwlkext2edg  29983  wwlksext2clwwlk  29984  clwlknf1oclwwlknlem1  30008  3wlkdlem5  30090  3wlkdlem10  30096  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  numclwlk2lem2f  30304  ex-exp  30377  1nei  32660  psgnfzto1st  33062  cyc3fv2  33095  archirngz  33133  archiabllem2c  33139  cos9thpiminplylem1  33762  lmat22e12  33796  lmat22e21  33797  lmat22e22  33798  madjusmdetlem4  33807  fiblem  34376  fibp1  34379  fib2  34380  fib3  34381  ballotlem2  34467  ballotlemfc0  34471  ballotlemfcc  34472  signstfveq0  34555  chtvalz  34607  hgt750lem  34629  hgt750lem2  34630  subfacp1lem5  35152  dnibndlem13  36454  knoppndvlem12  36487  420gcd8e4  41965  3exp7  42012  3lexlogpow5ineq1  42013  aks4d1p1  42035  2np3bcnp1  42103  sn-0ne2  42396  flt0  42607  fltnltalem  42632  rabren3dioph  42785  pellfundgt1  42853  areaquad  43187  resqrtvalex  43616  imsqrtvalex  43617  trclfvdecomr  43699  xralrple2  45329  sumnnodd  45607  itgsin0pilem1  45927  itgsinexp  45932  stoweidlem14  45991  stoweidlem26  46003  wallispilem3  46044  stirlinglem6  46056  stirlinglem11  46061  dirkertrigeqlem1  46075  sqwvfourb  46206  fourierswlem  46207  addmodne  47321  fmtno5lem1  47515  fmtno5lem4  47518  257prm  47523  fmtnoprmfac1lem  47526  fmtnofac1  47532  127prm  47561  m11nprm  47563  lighneallem2  47568  proththd  47576  opoeALTV  47645  1oddALTV  47652  nnsum3primes4  47750  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  bgoldbtbndlem1  47767  grtriclwlk3  47905  cycl3grtrilem  47906  gpgprismgr4cycllem10  48051  oddinmgm  48098  fldivexpfllog2  48493  blen2  48513  ackval1  48609  ackval0012  48617