Definition df-2 12210

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 12202	. 2 class 2
2		c1 11029	. . 3 class 1
3		caddc 11031	. . 3 class +
4	2, 2, 3	co 7353	. 2 class (1 + 1)
5	1, 4	wceq 1540	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12220  2re  12221  2cn  12222  0le2  12249  2pos  12250  1p1e2  12267  2p2e4  12277  2times  12278  1p2e3  12285  3p2e5  12293  4p2e6  12295  5p2e7  12298  6p2e8  12301  7p2e9  12303  1lt2  12313  nneo  12579  6p6e12  12684  7p5e12  12687  8p2e10  12690  8p4e12  12692  9p2e11  12697  9p3e12  12698  5t2e10  12710  eluz2b1  12839  x2times  13220  fztp  13502  fz12pr  13503  fztpval  13508  fzo12sn  13670  fzosplitpr  13698  sqval  14040  fac2  14205  faclbnd4lem1  14219  bcp1m1  14246  hashprg  14321  hashgt23el  14350  hashge2el2difr  14407  swrds2  14866  iseralt  15611  binom11  15758  climcndslem1  15775  climcndslem2  15776  bpoly1  15977  bpolydiflem  15980  bpoly3  15984  bpoly4  15985  ege2le3  16016  ef4p  16041  efgt1p2  16042  eirrlem  16132  odd2np1lem  16270  opoe  16293  bitsfzolem  16364  isprm3  16613  prmind2  16615  dvdsnprmd  16620  2mulprm  16623  pockthlem  16836  pockthg  16837  prmunb  16845  prmreclem2  16848  4sqlem19  16894  vdwlem12  16923  prmgaplem8  16989  2expltfac  17023  gsumpr12val  18582  mulg2  18981  psgnunilem2  19393  efgs1b  19634  efgredlemc  19643  lt6abl  19793  abvtrivd  20736  m2detleiblem2  22532  clmvs2  25011  cphipval  25160  pjthlem1  25354  ovolunlem1a  25414  ovolicc1  25434  vitalilem2  25527  itgcnlem  25708  dveflem  25900  coskpi  26449  ang180lem3  26738  tanatan  26846  cosatan  26848  atantayl2  26865  emcllem7  26929  basellem3  27010  basellem5  27012  basellem8  27015  issqf  27063  ppi2  27097  ppi3  27098  cht2  27099  ppieq0  27103  ppiublem2  27131  chpeq0  27136  chtub  27140  chpub  27148  mersenne  27155  perfectlem2  27158  bcp1ctr  27207  bclbnd  27208  bposlem1  27212  bposlem2  27213  bposlem6  27217  lgslem1  27225  lgsval2lem  27235  lgsdir2lem2  27254  lgsdir2lem3  27255  lgsdirprm  27259  lgseisen  27307  m1lgs  27316  rplogsumlem1  27412  rplogsumlem2  27413  dchrisum0flb  27438  dchrisum0re  27441  mulog2sumlem2  27463  pntrmax  27492  pntpbnd2  27515  pntibndlem2  27519  pntlemg  27526  pntlemr  27530  axlowdimlem13  28918  clwlkclwwlklem2a  29961  1wlkdlem1  30100  upgr3v3e3cycl  30143  upgr4cycl4dv4e  30148  numclwlk2lem2f1o  30342  ex-fl  30410  1p1e2apr1  30429  vc2OLD  30531  ipval2  30670  ip2i  30791  hv2times  31024  pjhthlem1  31354  ho2times  31782  stm1addi  32208  staddi  32209  stadd3i  32211  addltmulALT  32409  threehalves  32874  usgrgt2cycl  35122  subfacp1lem1  35171  subfacp1lem5  35176  subfacp1lem6  35177  sin2h  37609  tan2h  37611  poimirlem25  37644  poimirlem27  37646  itg2addnclem3  37672  aks4d1p1p7  42067  facp2  42136  sn-1ne2  42258  remul02  42398  sn-0tie0  42444  3cubeslem3r  42680  pell14qrgapw  42869  rmydioph  43007  rmxdioph  43009  expdiophlem1  43014  expdiophlem2  43015  expdioph  43016  relexp2  43670  stoweidlem14  46015  wallispilem3  46068  wallispi2lem2  46073  fourierswlem  46231  difmodm1lt  47363  perfectALTVlem2  47726  sbgoldbo  47791  nnsum3primes4  47792  nnsum3primesgbe  47796  nnlog2ge0lt1  48571  itcoval2  48669  ackval2  48687  ackval42  48701