Definition df-2 12301

Description: Define the number 2. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-2	⊢ 2 = (1 + 1)

Detailed syntax breakdown of Definition df-2

Step	Hyp	Ref	Expression
1		c2 12293	. 2 class 2
2		c1 11128	. . 3 class 1
3		caddc 11130	. . 3 class +
4	2, 2, 3	co 7403	. 2 class (1 + 1)
5	1, 4	wceq 1540	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12311  2re  12312  2cn  12313  0le2  12340  2pos  12341  1p1e2  12363  2p2e4  12373  2times  12374  1p2e3  12381  3p2e5  12389  4p2e6  12391  5p2e7  12394  6p2e8  12397  7p2e9  12399  1lt2  12409  nneo  12675  6p6e12  12780  7p5e12  12783  8p2e10  12786  8p4e12  12788  9p2e11  12793  9p3e12  12794  5t2e10  12806  eluz2b1  12933  x2times  13313  fztp  13595  fz12pr  13596  fztpval  13601  fzo12sn  13762  fzosplitpr  13790  sqval  14130  fac2  14295  faclbnd4lem1  14309  bcp1m1  14336  hashprg  14411  hashgt23el  14440  hashge2el2difr  14497  swrds2  14957  iseralt  15699  binom11  15846  climcndslem1  15863  climcndslem2  15864  bpoly1  16065  bpolydiflem  16068  bpoly3  16072  bpoly4  16073  ege2le3  16104  ef4p  16129  efgt1p2  16130  eirrlem  16220  odd2np1lem  16357  opoe  16380  bitsfzolem  16451  isprm3  16700  prmind2  16702  dvdsnprmd  16707  2mulprm  16710  pockthlem  16923  pockthg  16924  prmunb  16932  prmreclem2  16935  4sqlem19  16981  vdwlem12  17010  prmgaplem8  17076  2expltfac  17110  gsumpr12val  18665  mulg2  19064  psgnunilem2  19474  efgs1b  19715  efgredlemc  19724  lt6abl  19874  abvtrivd  20790  m2detleiblem2  22564  clmvs2  25043  cphipval  25193  pjthlem1  25387  ovolunlem1a  25447  ovolicc1  25467  vitalilem2  25560  itgcnlem  25741  dveflem  25933  coskpi  26482  ang180lem3  26771  tanatan  26879  cosatan  26881  atantayl2  26898  emcllem7  26962  basellem3  27043  basellem5  27045  basellem8  27048  issqf  27096  ppi2  27130  ppi3  27131  cht2  27132  ppieq0  27136  ppiublem2  27164  chpeq0  27169  chtub  27173  chpub  27181  mersenne  27188  perfectlem2  27191  bcp1ctr  27240  bclbnd  27241  bposlem1  27245  bposlem2  27246  bposlem6  27250  lgslem1  27258  lgsval2lem  27268  lgsdir2lem2  27287  lgsdir2lem3  27288  lgsdirprm  27292  lgseisen  27340  m1lgs  27349  rplogsumlem1  27445  rplogsumlem2  27446  dchrisum0flb  27471  dchrisum0re  27474  mulog2sumlem2  27496  pntrmax  27525  pntpbnd2  27548  pntibndlem2  27552  pntlemg  27559  pntlemr  27563  axlowdimlem13  28879  clwlkclwwlklem2a  29925  1wlkdlem1  30064  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  numclwlk2lem2f1o  30306  ex-fl  30374  1p1e2apr1  30393  vc2OLD  30495  ipval2  30634  ip2i  30755  hv2times  30988  pjhthlem1  31318  ho2times  31746  stm1addi  32172  staddi  32173  stadd3i  32175  addltmulALT  32373  threehalves  32835  usgrgt2cycl  35098  subfacp1lem1  35147  subfacp1lem5  35152  subfacp1lem6  35153  sin2h  37580  tan2h  37582  poimirlem25  37615  poimirlem27  37617  itg2addnclem3  37643  aks4d1p1p7  42033  facp2  42102  fac2xp3  42198  sn-1ne2  42262  remul02  42395  sn-0tie0  42429  3cubeslem3r  42657  pell14qrgapw  42846  rmydioph  42985  rmxdioph  42987  expdiophlem1  42992  expdiophlem2  42993  expdioph  42994  relexp2  43648  stoweidlem14  45991  wallispilem3  46044  wallispi2lem2  46049  fourierswlem  46207  perfectALTVlem2  47684  sbgoldbo  47749  nnsum3primes4  47750  nnsum3primesgbe  47754  difmodm1lt  48450  nnlog2ge0lt1  48494  itcoval2  48592  ackval2  48610  ackval42  48624