Theorem 1p1e2 12301

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

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  2c2 12236

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 2708

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

This theorem is referenced by:  2m1e1  12302  1p2e3  12319  add1p1  12428  sub1m1  12429  nn0n0n1ge2  12505  3halfnz  12608  10p10e20  12739  5t4e20  12746  6t4e24  12750  7t3e21  12754  8t3e24  12760  9t3e27  12767  fz12pr  13535  fz0to3un2pr  13583  fzo13pr  13704  fzo1to4tp  13709  fldiv4p1lem1div2  13794  m1modge3gt1  13880  fac2  14241  hash2  14367  hashprlei  14430  ccat2s1len  14586  ccat2s1p2  14593  s2len  14851  repsw2  14912  swrd2lsw  14914  2swrd2eqwrdeq  14915  nn0o1gt2  16350  3lcm2e6woprm  16584  ge2nprmge4  16671  2exp8  17059  2exp11  17060  2exp16  17061  prmlem0  17076  prmlem2  17090  37prm  17091  43prm  17092  83prm  17093  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem2  17112  4001lem3  17113  4001lem4  17114  m2detleiblem2  22593  logbleb  26747  logblt  26748  log2ublem3  26912  log2ub  26913  1sgm2ppw  27163  2sqb  27395  2sq2  27396  rplogsumlem2  27448  tgldimor  28570  1loopgrvd2  29572  2wlklem  29734  pthdlem1  29834  pthdlem2  29836  wwlksnextwrd  29965  wwlksnextproplem3  29979  2wlkdlem5  29997  2wlkdlem10  30003  rusgrnumwwlkl1  30039  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwwlkext2edg  30126  wwlksext2clwwlk  30127  clwlknf1oclwwlknlem1  30151  3wlkdlem5  30233  3wlkdlem10  30239  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  numclwlk2lem2f  30447  ex-exp  30520  1nei  32810  psgnfzto1st  33166  cyc3fv2  33199  archirngz  33250  archiabllem2c  33256  cos9thpiminplylem1  33926  lmat22e12  33963  lmat22e21  33964  lmat22e22  33965  madjusmdetlem4  33974  fiblem  34542  fibp1  34545  fib2  34546  fib3  34547  ballotlem2  34633  ballotlemfc0  34637  ballotlemfcc  34638  signstfveq0  34721  chtvalz  34773  hgt750lem  34795  hgt750lem2  34796  subfacp1lem5  35366  dnibndlem13  36750  knoppndvlem12  36783  420gcd8e4  42445  3exp7  42492  3lexlogpow5ineq1  42493  aks4d1p1  42515  2np3bcnp1  42583  sn-0ne2  42838  flt0  43070  fltnltalem  43095  rabren3dioph  43243  pellfundgt1  43311  areaquad  43644  resqrtvalex  44072  imsqrtvalex  44073  trclfvdecomr  44155  xralrple2  45784  sumnnodd  46060  itgsin0pilem1  46378  itgsinexp  46383  stoweidlem14  46442  stoweidlem26  46454  wallispilem3  46495  stirlinglem6  46507  stirlinglem11  46512  dirkertrigeqlem1  46526  sqwvfourb  46657  fourierswlem  46658  addmodne  47798  fmtno5lem1  48016  fmtno5lem4  48019  257prm  48024  fmtnoprmfac1lem  48027  fmtnofac1  48033  127prm  48062  m11nprm  48064  lighneallem2  48069  proththd  48077  opoeALTV  48159  1oddALTV  48166  nnsum3primes4  48264  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  bgoldbtbndlem1  48281  grtriclwlk3  48421  cycl3grtrilem  48422  gpgprismgr4cycllem10  48580  oddinmgm  48651  fldivexpfllog2  49041  blen2  49061  ackval1  49157  ackval0012  49165