Theorem 1p1e2 12282

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

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  2c2 12217

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  2m1e1  12283  1p2e3  12300  add1p1  12409  sub1m1  12410  nn0n0n1ge2  12486  3halfnz  12589  10p10e20  12720  5t4e20  12727  6t4e24  12731  7t3e21  12735  8t3e24  12741  9t3e27  12748  fz12pr  13518  fz0to3un2pr  13566  fzo13pr  13686  fzo1to4tp  13691  fldiv4p1lem1div2  13773  m1modge3gt1  13859  fac2  14220  hash2  14346  hashprlei  14409  ccat2s1len  14564  ccat2s1p2  14571  s2len  14831  repsw2  14892  swrd2lsw  14894  2swrd2eqwrdeq  14895  nn0o1gt2  16327  3lcm2e6woprm  16561  ge2nprmge4  16647  2exp8  17035  2exp11  17036  2exp16  17037  prmlem0  17052  prmlem2  17066  37prm  17067  43prm  17068  83prm  17069  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem4  17080  1259lem5  17081  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem2  17088  4001lem3  17089  4001lem4  17090  m2detleiblem2  22548  logbleb  26726  logblt  26727  log2ublem3  26891  log2ub  26892  1sgm2ppw  27144  2sqb  27376  2sq2  27377  rplogsumlem2  27429  tgldimor  28482  1loopgrvd2  29484  2wlklem  29646  pthdlem1  29746  pthdlem2  29748  wwlksnextwrd  29877  wwlksnextproplem3  29891  2wlkdlem5  29909  2wlkdlem10  29915  rusgrnumwwlkl1  29948  clwlkclwwlklem2a4  29976  clwlkclwwlklem2a  29977  clwwlkext2edg  30035  wwlksext2clwwlk  30036  clwlknf1oclwwlknlem1  30060  3wlkdlem5  30142  3wlkdlem10  30148  upgr3v3e3cycl  30159  upgr4cycl4dv4e  30164  konigsberglem1  30231  konigsberglem2  30232  konigsberglem3  30233  numclwlk2lem2f  30356  ex-exp  30429  1nei  32710  psgnfzto1st  33077  cyc3fv2  33110  archirngz  33158  archiabllem2c  33164  cos9thpiminplylem1  33765  lmat22e12  33802  lmat22e21  33803  lmat22e22  33804  madjusmdetlem4  33813  fiblem  34382  fibp1  34385  fib2  34386  fib3  34387  ballotlem2  34473  ballotlemfc0  34477  ballotlemfcc  34478  signstfveq0  34561  chtvalz  34613  hgt750lem  34635  hgt750lem2  34636  subfacp1lem5  35164  dnibndlem13  36471  knoppndvlem12  36504  420gcd8e4  41987  3exp7  42034  3lexlogpow5ineq1  42035  aks4d1p1  42057  2np3bcnp1  42125  sn-0ne2  42387  flt0  42618  fltnltalem  42643  rabren3dioph  42796  pellfundgt1  42864  areaquad  43198  resqrtvalex  43627  imsqrtvalex  43628  trclfvdecomr  43710  xralrple2  45343  sumnnodd  45621  itgsin0pilem1  45941  itgsinexp  45946  stoweidlem14  46005  stoweidlem26  46017  wallispilem3  46058  stirlinglem6  46070  stirlinglem11  46075  dirkertrigeqlem1  46089  sqwvfourb  46220  fourierswlem  46221  addmodne  47338  fmtno5lem1  47547  fmtno5lem4  47550  257prm  47555  fmtnoprmfac1lem  47558  fmtnofac1  47564  127prm  47593  m11nprm  47595  lighneallem2  47600  proththd  47608  opoeALTV  47677  1oddALTV  47684  nnsum3primes4  47782  nnsum3primesgbe  47786  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  bgoldbtbndlem1  47799  grtriclwlk3  47937  cycl3grtrilem  47938  gpgprismgr4cycllem10  48087  oddinmgm  48156  fldivexpfllog2  48547  blen2  48567  ackval1  48663  ackval0012  48671