Theorem 1p1e2 12296

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

Syntax hints:   = wceq 1542  (class class class)co 7362  1c1 11034   + caddc 11036  2c2 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-2 12239

This theorem is referenced by:  2m1e1  12297  1p2e3  12314  add1p1  12423  sub1m1  12424  nn0n0n1ge2  12500  3halfnz  12603  10p10e20  12734  5t4e20  12741  6t4e24  12745  7t3e21  12749  8t3e24  12755  9t3e27  12762  fz12pr  13530  fz0to3un2pr  13578  fzo13pr  13699  fzo1to4tp  13704  fldiv4p1lem1div2  13789  m1modge3gt1  13875  fac2  14236  hash2  14362  hashprlei  14425  ccat2s1len  14581  ccat2s1p2  14588  s2len  14846  repsw2  14907  swrd2lsw  14909  2swrd2eqwrdeq  14910  nn0o1gt2  16345  3lcm2e6woprm  16579  ge2nprmge4  16666  2exp8  17054  2exp11  17055  2exp16  17056  prmlem0  17071  prmlem2  17085  37prm  17086  43prm  17087  83prm  17088  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem4  17099  1259lem5  17100  2503lem1  17102  2503lem2  17103  2503lem3  17104  2503prm  17105  4001lem2  17107  4001lem3  17108  4001lem4  17109  m2detleiblem2  22607  logbleb  26764  logblt  26765  log2ublem3  26929  log2ub  26930  1sgm2ppw  27181  2sqb  27413  2sq2  27414  rplogsumlem2  27466  tgldimor  28588  1loopgrvd2  29591  2wlklem  29753  pthdlem1  29853  pthdlem2  29855  wwlksnextwrd  29984  wwlksnextproplem3  29998  2wlkdlem5  30016  2wlkdlem10  30022  rusgrnumwwlkl1  30058  clwlkclwwlklem2a4  30086  clwlkclwwlklem2a  30087  clwwlkext2edg  30145  wwlksext2clwwlk  30146  clwlknf1oclwwlknlem1  30170  3wlkdlem5  30252  3wlkdlem10  30258  upgr3v3e3cycl  30269  upgr4cycl4dv4e  30274  konigsberglem1  30341  konigsberglem2  30342  konigsberglem3  30343  numclwlk2lem2f  30466  ex-exp  30539  1nei  32829  psgnfzto1st  33185  cyc3fv2  33218  archirngz  33269  archiabllem2c  33275  cos9thpiminplylem1  33946  lmat22e12  33983  lmat22e21  33984  lmat22e22  33985  madjusmdetlem4  33994  fiblem  34562  fibp1  34565  fib2  34566  fib3  34567  ballotlem2  34653  ballotlemfc0  34657  ballotlemfcc  34658  signstfveq0  34741  chtvalz  34793  hgt750lem  34815  hgt750lem2  34816  subfacp1lem5  35386  dnibndlem13  36770  knoppndvlem12  36803  420gcd8e4  42463  3exp7  42510  3lexlogpow5ineq1  42511  aks4d1p1  42533  2np3bcnp1  42601  sn-0ne2  42856  flt0  43088  fltnltalem  43113  rabren3dioph  43265  pellfundgt1  43333  areaquad  43666  resqrtvalex  44094  imsqrtvalex  44095  trclfvdecomr  44177  xralrple2  45806  sumnnodd  46082  itgsin0pilem1  46400  itgsinexp  46405  stoweidlem14  46464  stoweidlem26  46476  wallispilem3  46517  stirlinglem6  46529  stirlinglem11  46534  dirkertrigeqlem1  46548  sqwvfourb  46679  fourierswlem  46680  addmodne  47814  fmtno5lem1  48032  fmtno5lem4  48035  257prm  48040  fmtnoprmfac1lem  48043  fmtnofac1  48049  127prm  48078  m11nprm  48080  lighneallem2  48085  proththd  48093  opoeALTV  48175  1oddALTV  48182  nnsum3primes4  48280  nnsum3primesgbe  48284  nnsum4primesodd  48288  nnsum4primesoddALTV  48289  bgoldbtbndlem1  48297  grtriclwlk3  48437  cycl3grtrilem  48438  gpgprismgr4cycllem10  48596  oddinmgm  48667  fldivexpfllog2  49057  blen2  49077  ackval1  49173  ackval0012  49181