Theorem 1p1e2 12293

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

Syntax hints:   = wceq 1547  (class class class)co 7357  1c1 11031   + caddc 11033  2c2 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-2 12236

This theorem is referenced by:  2m1e1  12294  1p2e3  12311  add1p1  12420  sub1m1  12421  nn0n0n1ge2  12497  3halfnz  12600  10p10e20  12731  5t4e20  12738  6t4e24  12742  7t3e21  12746  8t3e24  12752  9t3e27  12759  fz12pr  13527  fz0to3un2pr  13575  fzo13pr  13696  fzo1to4tp  13701  fldiv4p1lem1div2  13786  m1modge3gt1  13872  fac2  14233  hash2  14359  hashprlei  14422  ccat2s1len  14578  ccat2s1p2  14585  s2len  14843  repsw2  14904  swrd2lsw  14906  2swrd2eqwrdeq  14907  nn0o1gt2  16342  3lcm2e6woprm  16576  ge2nprmge4  16663  2exp8  17051  2exp11  17052  2exp16  17053  prmlem0  17068  prmlem2  17082  37prm  17083  43prm  17084  83prm  17085  317prm  17088  631prm  17089  1259lem1  17093  1259lem2  17094  1259lem4  17096  1259lem5  17097  2503lem1  17099  2503lem2  17100  2503lem3  17101  2503prm  17102  4001lem2  17104  4001lem3  17105  4001lem4  17106  m2detleiblem2  22612  logbleb  26766  logblt  26767  log2ublem3  26931  log2ub  26932  1sgm2ppw  27182  2sqb  27414  2sq2  27415  rplogsumlem2  27467  tgldimor  28589  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  32830  psgnfzto1st  33187  cyc3fv2  33220  archirngz  33271  archiabllem2c  33277  cos9thpiminplylem1  33975  lmat22e12  34012  lmat22e21  34013  lmat22e22  34014  madjusmdetlem4  34023  fiblem  34591  fibp1  34594  fib2  34595  fib3  34596  ballotlem2  34682  ballotlemfc0  34686  ballotlemfcc  34687  signstfveq0  34770  chtvalz  34822  hgt750lem  34844  hgt750lem2  34845  subfacp1lem5  35421  dnibndlem13  36805  knoppndvlem12  36838  420gcd8e4  42500  3exp7  42547  3lexlogpow5ineq1  42548  aks4d1p1  42570  2np3bcnp1  42638  sn-0ne2  42892  flt0  43096  fltnltalem  43121  rabren3dioph  43269  pellfundgt1  43337  areaquad  43670  resqrtvalex  44098  imsqrtvalex  44099  trclfvdecomr  44181  xralrple2  45807  sumnnodd  46083  itgsin0pilem1  46401  itgsinexp  46406  stoweidlem14  46465  stoweidlem26  46477  wallispilem3  46518  stirlinglem6  46530  stirlinglem11  46535  dirkertrigeqlem1  46549  sqwvfourb  46680  fourierswlem  46681  addmodne  47821  fmtno5lem1  48039  fmtno5lem4  48042  257prm  48047  fmtnoprmfac1lem  48050  fmtnofac1  48056  127prm  48085  m11nprm  48087  lighneallem2  48092  proththd  48100  opoeALTV  48182  1oddALTV  48189  nnsum3primes4  48287  nnsum3primesgbe  48291  nnsum4primesodd  48295  nnsum4primesoddALTV  48296  bgoldbtbndlem1  48304  grtriclwlk3  48444  cycl3grtrilem  48445  gpgprismgr4cycllem10  48603  oddinmgm  48674  fldivexpfllog2  49064  blen2  49084  ackval1  49180  ackval0012  49188