Theorem 1p1e2 12313

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

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078  2c2 12248

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 2702

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

This theorem is referenced by:  2m1e1  12314  1p2e3  12331  add1p1  12440  sub1m1  12441  nn0n0n1ge2  12517  3halfnz  12620  10p10e20  12751  5t4e20  12758  6t4e24  12762  7t3e21  12766  8t3e24  12772  9t3e27  12779  fz12pr  13549  fz0to3un2pr  13597  fzo13pr  13717  fzo1to4tp  13722  fldiv4p1lem1div2  13804  m1modge3gt1  13890  fac2  14251  hash2  14377  hashprlei  14440  ccat2s1len  14595  ccat2s1p2  14602  s2len  14862  repsw2  14923  swrd2lsw  14925  2swrd2eqwrdeq  14926  nn0o1gt2  16358  3lcm2e6woprm  16592  ge2nprmge4  16678  2exp8  17066  2exp11  17067  2exp16  17068  prmlem0  17083  prmlem2  17097  37prm  17098  43prm  17099  83prm  17100  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem2  17119  4001lem3  17120  4001lem4  17121  m2detleiblem2  22522  logbleb  26700  logblt  26701  log2ublem3  26865  log2ub  26866  1sgm2ppw  27118  2sqb  27350  2sq2  27351  rplogsumlem2  27403  tgldimor  28436  1loopgrvd2  29438  2wlklem  29602  pthdlem1  29703  pthdlem2  29705  wwlksnextwrd  29834  wwlksnextproplem3  29848  2wlkdlem5  29866  2wlkdlem10  29872  rusgrnumwwlkl1  29905  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwwlkext2edg  29992  wwlksext2clwwlk  29993  clwlknf1oclwwlknlem1  30017  3wlkdlem5  30099  3wlkdlem10  30105  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  numclwlk2lem2f  30313  ex-exp  30386  1nei  32667  psgnfzto1st  33069  cyc3fv2  33102  archirngz  33150  archiabllem2c  33156  cos9thpiminplylem1  33779  lmat22e12  33816  lmat22e21  33817  lmat22e22  33818  madjusmdetlem4  33827  fiblem  34396  fibp1  34399  fib2  34400  fib3  34401  ballotlem2  34487  ballotlemfc0  34491  ballotlemfcc  34492  signstfveq0  34575  chtvalz  34627  hgt750lem  34649  hgt750lem2  34650  subfacp1lem5  35178  dnibndlem13  36485  knoppndvlem12  36518  420gcd8e4  42001  3exp7  42048  3lexlogpow5ineq1  42049  aks4d1p1  42071  2np3bcnp1  42139  sn-0ne2  42401  flt0  42632  fltnltalem  42657  rabren3dioph  42810  pellfundgt1  42878  areaquad  43212  resqrtvalex  43641  imsqrtvalex  43642  trclfvdecomr  43724  xralrple2  45357  sumnnodd  45635  itgsin0pilem1  45955  itgsinexp  45960  stoweidlem14  46019  stoweidlem26  46031  wallispilem3  46072  stirlinglem6  46084  stirlinglem11  46089  dirkertrigeqlem1  46103  sqwvfourb  46234  fourierswlem  46235  addmodne  47349  fmtno5lem1  47558  fmtno5lem4  47561  257prm  47566  fmtnoprmfac1lem  47569  fmtnofac1  47575  127prm  47604  m11nprm  47606  lighneallem2  47611  proththd  47619  opoeALTV  47688  1oddALTV  47695  nnsum3primes4  47793  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  bgoldbtbndlem1  47810  grtriclwlk3  47948  cycl3grtrilem  47949  gpgprismgr4cycllem10  48098  oddinmgm  48167  fldivexpfllog2  48558  blen2  48578  ackval1  48674  ackval0012  48682