Definition df-2 12239

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 12231	. 2 class 2
2		c1 11035	. . 3 class 1
3		caddc 11037	. . 3 class +
4	2, 2, 3	co 7359	. 2 class (1 + 1)
5	1, 4	wceq 1548	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12249  2re  12250  2cn  12251  0le2  12278  2pos  12279  1p1e2  12296  2p2e4  12306  2times  12307  1p2e3  12314  3p2e5  12322  4p2e6  12324  5p2e7  12327  6p2e8  12330  7p2e9  12332  1lt2  12342  nneo  12608  6p6e12  12713  7p5e12  12716  8p2e10  12719  8p4e12  12721  9p2e11  12726  9p3e12  12727  5t2e10  12739  eluz2b1  12864  x2times  13246  fztp  13529  fz12pr  13530  fztpval  13535  fzo12sn  13698  fzosplitpr  13727  sqval  14071  fac2  14236  faclbnd4lem1  14250  bcp1m1  14277  hashprg  14352  hashgt23el  14381  hashge2el2difr  14438  swrds2  14897  iseralt  15642  binom11  15792  climcndslem1  15809  climcndslem2  15810  bpoly1  16011  bpolydiflem  16014  bpoly3  16018  bpoly4  16019  ege2le3  16050  ef4p  16075  efgt1p2  16076  eirrlem  16166  odd2np1lem  16304  opoe  16327  bitsfzolem  16398  isprm3  16647  prmind2  16649  dvdsnprmd  16654  2mulprm  16657  pockthlem  16871  pockthg  16872  prmunb  16880  prmreclem2  16883  4sqlem19  16929  vdwlem12  16958  prmgaplem8  17024  2expltfac  17058  gsumpr12val  18652  mulg2  19054  psgnunilem2  19464  efgs1b  19705  efgredlemc  19714  lt6abl  19864  abvtrivd  20807  m2detleiblem2  22614  clmvs2  25082  cphipval  25231  pjthlem1  25425  ovolunlem1a  25484  ovolicc1  25504  vitalilem2  25597  itgcnlem  25778  dveflem  25967  coskpi  26508  ang180lem3  26796  tanatan  26904  cosatan  26906  atantayl2  26923  emcllem7  26986  basellem3  27067  basellem5  27069  basellem8  27072  issqf  27120  ppi2  27154  ppi3  27155  cht2  27156  ppieq0  27160  ppiublem2  27187  chpeq0  27192  chtub  27196  chpub  27204  mersenne  27211  perfectlem2  27214  bcp1ctr  27263  bclbnd  27264  bposlem1  27268  bposlem2  27269  bposlem6  27273  lgslem1  27281  lgsval2lem  27291  lgsdir2lem2  27310  lgsdir2lem3  27311  lgsdirprm  27315  lgseisen  27363  m1lgs  27372  rplogsumlem1  27468  rplogsumlem2  27469  dchrisum0flb  27494  dchrisum0re  27497  mulog2sumlem2  27519  pntrmax  27548  pntpbnd2  27571  pntibndlem2  27575  pntlemg  27582  pntlemr  27586  axlowdimlem13  29043  clwlkclwwlklem2a  30088  1wlkdlem1  30227  upgr3v3e3cycl  30270  upgr4cycl4dv4e  30275  numclwlk2lem2f1o  30469  ex-fl  30537  1p1e2apr1  30556  vc2OLD  30659  ipval2  30798  ip2i  30919  hv2times  31152  pjhthlem1  31482  ho2times  31910  stm1addi  32336  staddi  32337  stadd3i  32339  addltmulALT  32537  threehalves  32995  usgrgt2cycl  35371  subfacp1lem1  35420  subfacp1lem5  35425  subfacp1lem6  35426  sin2h  37990  tan2h  37992  poimirlem25  38025  poimirlem27  38027  itg2addnclem3  38053  aks4d1p1p7  42572  facp2  42641  sn-1ne2  42761  remul02  42895  sn-0tie0  42954  3cubeslem3r  43149  pell14qrgapw  43334  rmydioph  43472  rmxdioph  43474  expdiophlem1  43479  expdiophlem2  43480  expdioph  43481  relexp2  44134  stoweidlem14  46469  wallispilem3  46522  wallispi2lem2  46527  fourierswlem  46685  difmodm1lt  47840  perfectALTVlem2  48225  sbgoldbo  48290  nnsum3primes4  48291  nnsum3primesgbe  48295  nnlog2ge0lt1  49069  itcoval2  49167  ackval2  49185  ackval42  49199