Definition df-2 12329

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 12321	. 2 class 2
2		c1 11156	. . 3 class 1
3		caddc 11158	. . 3 class +
4	2, 2, 3	co 7431	. 2 class (1 + 1)
5	1, 4	wceq 1540	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12339  2re  12340  2cn  12341  0le2  12368  2pos  12369  1p1e2  12391  2p2e4  12401  2times  12402  1p2e3  12409  3p2e5  12417  4p2e6  12419  5p2e7  12422  6p2e8  12425  7p2e9  12427  1lt2  12437  nneo  12702  6p6e12  12807  7p5e12  12810  8p2e10  12813  8p4e12  12815  9p2e11  12820  9p3e12  12821  5t2e10  12833  eluz2b1  12961  x2times  13341  fztp  13620  fz12pr  13621  fztpval  13626  fzo12sn  13787  fzosplitpr  13815  sqval  14155  fac2  14318  faclbnd4lem1  14332  bcp1m1  14359  hashprg  14434  hashgt23el  14463  hashge2el2difr  14520  swrds2  14979  iseralt  15721  binom11  15868  climcndslem1  15885  climcndslem2  15886  bpoly1  16087  bpolydiflem  16090  bpoly3  16094  bpoly4  16095  ege2le3  16126  ef4p  16149  efgt1p2  16150  eirrlem  16240  odd2np1lem  16377  opoe  16400  bitsfzolem  16471  isprm3  16720  prmind2  16722  dvdsnprmd  16727  2mulprm  16730  pockthlem  16943  pockthg  16944  prmunb  16952  prmreclem2  16955  4sqlem19  17001  vdwlem12  17030  prmgaplem8  17096  2expltfac  17130  gsumpr12val  18702  mulg2  19101  psgnunilem2  19513  efgs1b  19754  efgredlemc  19763  lt6abl  19913  abvtrivd  20833  m2detleiblem2  22634  clmvs2  25127  cphipval  25277  pjthlem1  25471  ovolunlem1a  25531  ovolicc1  25551  vitalilem2  25644  itgcnlem  25825  dveflem  26017  coskpi  26565  ang180lem3  26854  tanatan  26962  cosatan  26964  atantayl2  26981  emcllem7  27045  basellem3  27126  basellem5  27128  basellem8  27131  issqf  27179  ppi2  27213  ppi3  27214  cht2  27215  ppieq0  27219  ppiublem2  27247  chpeq0  27252  chtub  27256  chpub  27264  mersenne  27271  perfectlem2  27274  bcp1ctr  27323  bclbnd  27324  bposlem1  27328  bposlem2  27329  bposlem6  27333  lgslem1  27341  lgsval2lem  27351  lgsdir2lem2  27370  lgsdir2lem3  27371  lgsdirprm  27375  lgseisen  27423  m1lgs  27432  rplogsumlem1  27528  rplogsumlem2  27529  dchrisum0flb  27554  dchrisum0re  27557  mulog2sumlem2  27579  pntrmax  27608  pntpbnd2  27631  pntibndlem2  27635  pntlemg  27642  pntlemr  27646  axlowdimlem13  28969  clwlkclwwlklem2a  30017  1wlkdlem1  30156  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  numclwlk2lem2f1o  30398  ex-fl  30466  1p1e2apr1  30485  vc2OLD  30587  ipval2  30726  ip2i  30847  hv2times  31080  pjhthlem1  31410  ho2times  31838  stm1addi  32264  staddi  32265  stadd3i  32267  addltmulALT  32465  threehalves  32897  usgrgt2cycl  35135  subfacp1lem1  35184  subfacp1lem5  35189  subfacp1lem6  35190  sin2h  37617  tan2h  37619  poimirlem25  37652  poimirlem27  37654  itg2addnclem3  37680  aks4d1p1p7  42075  facp2  42144  fac2xp3  42240  sn-1ne2  42300  remul02  42435  sn-0tie0  42469  3cubeslem3r  42698  pell14qrgapw  42887  rmydioph  43026  rmxdioph  43028  expdiophlem1  43033  expdiophlem2  43034  expdioph  43035  relexp2  43690  stoweidlem14  46029  wallispilem3  46082  wallispi2lem2  46087  fourierswlem  46245  perfectALTVlem2  47709  sbgoldbo  47774  nnsum3primes4  47775  nnsum3primesgbe  47779  difmodm1lt  48443  nnlog2ge0lt1  48487  itcoval2  48585  ackval2  48603  ackval42  48617