Theorem 1p1e2 12343

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

Syntax hints:   = wceq 1562  (class class class)co 7398  1c1 11076   + caddc 11078  2c2 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-2 12282

This theorem is referenced by:  2m1e1OLD  12345  1p2e3  12362  add1p1  12474  sub1m1  12475  nn0n0n1ge2  12551  3halfnz  12654  10p10e20  12790  5t4e20  12797  6t4e24  12801  7t3e21  12805  8t3e24  12811  9t3e27  12818  fz12pr  13588  fz0to3un2pr  13636  fzo13pr  13757  fzo1to4tp  13762  fldiv4p1lem1div2  13847  m1modge3gt1  13933  fac2  14294  hash2  14420  hashprlei  14483  ccat2s1len  14639  ccat2s1p2  14646  s2len  14904  repsw2  14965  swrd2lsw  14967  2swrd2eqwrdeq  14968  nn0o1gt2  16417  3lcm2e6woprm  16651  ge2nprmge4  16738  2exp8  17126  2exp11  17127  2exp16  17128  prmlem0  17143  prmlem2  17158  37prm  17159  43prm  17160  83prm  17161  317prm  17164  631prm  17165  1259lem1  17169  1259lem2  17170  1259lem4  17172  1259lem5  17173  2503lem1  17175  2503lem2  17176  2503lem3  17177  2503prm  17178  4001lem2  17180  4001lem3  17181  4001lem4  17182  m2detleiblem2  22690  logbleb  26850  logblt  26851  log2ublem3  27015  log2ub  27016  1sgm2ppw  27266  2sqb  27498  2sq2  27499  rplogsumlem2  27551  tgldimor  28673  1loopgrvd2  29706  2wlklem  29868  pthdlem1  29968  pthdlem2  29970  wwlksnextwrd  30099  wwlksnextproplem3  30113  2wlkdlem5  30131  2wlkdlem10  30137  rusgrnumwwlkl1  30173  clwlkclwwlklem2a4  30201  clwlkclwwlklem2a  30202  clwwlkext2edg  30260  wwlksext2clwwlk  30261  clwlknf1oclwwlknlem1  30285  3wlkdlem5  30367  3wlkdlem10  30373  upgr3v3e3cycl  30384  upgr4cycl4dv4e  30389  konigsberglem1  30456  konigsberglem2  30457  konigsberglem3  30458  numclwlk2lem2f  30581  ex-exp  30654  1nei  32941  psgnfzto1st  33287  cyc3fv2  33320  archirngz  33371  archiabllem2c  33377  cos9thpiminplylem1  34081  lmat22e12  34118  lmat22e21  34119  lmat22e22  34120  madjusmdetlem4  34129  fiblem  34697  fibp1  34700  fib2  34701  fib3  34702  ballotlem2  34788  ballotlemfc0  34792  ballotlemfcc  34793  signstfveq0  34873  chtvalz  34925  hgt750lem  34947  hgt750lem2  34948  subfacp1lem5  35539  dnibndlem13  36933  knoppndvlem12  36966  420gcd8e4  42628  3exp7  42675  3lexlogpow5ineq1  42676  aks4d1p1  42698  2np3bcnp1  42766  sn-0ne2  43020  flt0  43224  fltnltalem  43249  rabren3dioph  43397  pellfundgt1  43465  areaquad  43798  resqrtvalex  44226  imsqrtvalex  44227  trclfvdecomr  44309  xralrple2  45935  sumnnodd  46211  itgsin0pilem1  46529  itgsinexp  46534  stoweidlem14  46593  stoweidlem26  46605  wallispilem3  46646  stirlinglem6  46658  stirlinglem11  46663  dirkertrigeqlem1  46677  sqwvfourb  46808  fourierswlem  46809  addmodne  47949  fmtno5lem1  48167  fmtno5lem4  48170  257prm  48175  fmtnoprmfac1lem  48178  fmtnofac1  48184  127prm  48213  m11nprm  48215  lighneallem2  48220  proththd  48228  opoeALTV  48310  1oddALTV  48317  nnsum3primes4  48415  nnsum3primesgbe  48419  nnsum4primesodd  48423  nnsum4primesoddALTV  48424  bgoldbtbndlem1  48432  grtriclwlk3  48572  cycl3grtrilem  48573  gpgprismgr4cycllem10  48731  oddinmgm  48802  fldivexpfllog2  49192  blen2  49212  ackval1  49308  ackval0012  49316