Theorem 1p1e2 12306

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  2c2 12241

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 2701

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

This theorem is referenced by:  2m1e1  12307  1p2e3  12324  add1p1  12433  sub1m1  12434  nn0n0n1ge2  12510  3halfnz  12613  10p10e20  12744  5t4e20  12751  6t4e24  12755  7t3e21  12759  8t3e24  12765  9t3e27  12772  fz12pr  13542  fz0to3un2pr  13590  fzo13pr  13710  fzo1to4tp  13715  fldiv4p1lem1div2  13797  m1modge3gt1  13883  fac2  14244  hash2  14370  hashprlei  14433  ccat2s1len  14588  ccat2s1p2  14595  s2len  14855  repsw2  14916  swrd2lsw  14918  2swrd2eqwrdeq  14919  nn0o1gt2  16351  3lcm2e6woprm  16585  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  22515  logbleb  26693  logblt  26694  log2ublem3  26858  log2ub  26859  1sgm2ppw  27111  2sqb  27343  2sq2  27344  rplogsumlem2  27396  tgldimor  28429  1loopgrvd2  29431  2wlklem  29595  pthdlem1  29696  pthdlem2  29698  wwlksnextwrd  29827  wwlksnextproplem3  29841  2wlkdlem5  29859  2wlkdlem10  29865  rusgrnumwwlkl1  29898  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwwlkext2edg  29985  wwlksext2clwwlk  29986  clwlknf1oclwwlknlem1  30010  3wlkdlem5  30092  3wlkdlem10  30098  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  numclwlk2lem2f  30306  ex-exp  30379  1nei  32660  psgnfzto1st  33062  cyc3fv2  33095  archirngz  33143  archiabllem2c  33149  cos9thpiminplylem1  33772  lmat22e12  33809  lmat22e21  33810  lmat22e22  33811  madjusmdetlem4  33820  fiblem  34389  fibp1  34392  fib2  34393  fib3  34394  ballotlem2  34480  ballotlemfc0  34484  ballotlemfcc  34485  signstfveq0  34568  chtvalz  34620  hgt750lem  34642  hgt750lem2  34643  subfacp1lem5  35171  dnibndlem13  36478  knoppndvlem12  36511  420gcd8e4  41994  3exp7  42041  3lexlogpow5ineq1  42042  aks4d1p1  42064  2np3bcnp1  42132  sn-0ne2  42394  flt0  42625  fltnltalem  42650  rabren3dioph  42803  pellfundgt1  42871  areaquad  43205  resqrtvalex  43634  imsqrtvalex  43635  trclfvdecomr  43717  xralrple2  45350  sumnnodd  45628  itgsin0pilem1  45948  itgsinexp  45953  stoweidlem14  46012  stoweidlem26  46024  wallispilem3  46065  stirlinglem6  46077  stirlinglem11  46082  dirkertrigeqlem1  46096  sqwvfourb  46227  fourierswlem  46228  addmodne  47345  fmtno5lem1  47554  fmtno5lem4  47557  257prm  47562  fmtnoprmfac1lem  47565  fmtnofac1  47571  127prm  47600  m11nprm  47602  lighneallem2  47607  proththd  47615  opoeALTV  47684  1oddALTV  47691  nnsum3primes4  47789  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  bgoldbtbndlem1  47806  grtriclwlk3  47944  cycl3grtrilem  47945  gpgprismgr4cycllem10  48094  oddinmgm  48163  fldivexpfllog2  48554  blen2  48574  ackval1  48670  ackval0012  48678