Theorem 1p1e2 12333

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

Syntax hints:   = wceq 1542  (class class class)co 7404  1c1 11107   + caddc 11109  2c2 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-2 12271

This theorem is referenced by:  2m1e1  12334  1p2e3  12351  add1p1  12459  sub1m1  12460  nn0n0n1ge2  12535  3halfnz  12637  10p10e20  12768  5t4e20  12775  6t4e24  12779  7t3e21  12783  8t3e24  12789  9t3e27  12796  fz12pr  13554  fz0to3un2pr  13599  fzo13pr  13712  fzo1to4tp  13716  fldiv4p1lem1div2  13796  m1modge3gt1  13879  fac2  14235  hash2  14361  hashprlei  14425  ccat2s1len  14569  ccat2s1p2  14576  s2len  14836  repsw2  14897  swrd2lsw  14899  2swrd2eqwrdeq  14900  nn0o1gt2  16320  3lcm2e6woprm  16548  ge2nprmge4  16634  2exp8  17018  2exp11  17019  2exp16  17020  prmlem0  17035  prmlem2  17049  37prm  17050  43prm  17051  83prm  17052  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem4  17063  1259lem5  17064  2503lem1  17066  2503lem2  17067  2503lem3  17068  2503prm  17069  4001lem2  17071  4001lem3  17072  4001lem4  17073  m2detleiblem2  22112  logbleb  26268  logblt  26269  log2ublem3  26433  log2ub  26434  1sgm2ppw  26683  2sqb  26915  2sq2  26916  rplogsumlem2  26968  tgldimor  27733  1loopgrvd2  28740  2wlklem  28904  pthdlem1  29003  pthdlem2  29005  wwlksnextwrd  29131  wwlksnextproplem3  29145  2wlkdlem5  29163  2wlkdlem10  29169  rusgrnumwwlkl1  29202  clwlkclwwlklem2a4  29230  clwlkclwwlklem2a  29231  clwwlkext2edg  29289  wwlksext2clwwlk  29290  clwlknf1oclwwlknlem1  29314  3wlkdlem5  29396  3wlkdlem10  29402  upgr3v3e3cycl  29413  upgr4cycl4dv4e  29418  konigsberglem1  29485  konigsberglem2  29486  konigsberglem3  29487  numclwlk2lem2f  29610  ex-exp  29683  1nei  31939  psgnfzto1st  32242  cyc3fv2  32275  archirngz  32313  archiabllem2c  32319  lmat22e12  32737  lmat22e21  32738  lmat22e22  32739  madjusmdetlem4  32748  fiblem  33335  fibp1  33338  fib2  33339  fib3  33340  ballotlem2  33425  ballotlemfc0  33429  ballotlemfcc  33430  signstfveq0  33526  chtvalz  33579  hgt750lem  33601  hgt750lem2  33602  subfacp1lem5  34113  dnibndlem13  35304  knoppndvlem12  35337  420gcd8e4  40809  3exp7  40856  3lexlogpow5ineq1  40857  aks4d1p1  40879  2np3bcnp1  40898  sn-0ne2  41223  flt0  41323  fltnltalem  41348  rabren3dioph  41486  pellfundgt1  41554  areaquad  41898  resqrtvalex  42329  imsqrtvalex  42330  trclfvdecomr  42412  xralrple2  43999  sumnnodd  44281  itgsin0pilem1  44601  itgsinexp  44606  stoweidlem14  44665  stoweidlem26  44677  wallispilem3  44718  stirlinglem6  44730  stirlinglem11  44735  dirkertrigeqlem1  44749  sqwvfourb  44880  fourierswlem  44881  fmtno5lem1  46156  fmtno5lem4  46159  257prm  46164  fmtnoprmfac1lem  46167  fmtnofac1  46173  127prm  46202  m11nprm  46204  lighneallem2  46209  proththd  46217  opoeALTV  46286  1oddALTV  46293  nnsum3primes4  46391  nnsum3primesgbe  46395  nnsum4primesodd  46399  nnsum4primesoddALTV  46400  bgoldbtbndlem1  46408  oddinmgm  46520  fldivexpfllog2  47153  blen2  47173  ackval1  47269  ackval0012  47277