Definition df-2 12183

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 12175	. 2 class 2
2		c1 11002	. . 3 class 1
3		caddc 11004	. . 3 class +
4	2, 2, 3	co 7341	. 2 class (1 + 1)
5	1, 4	wceq 1541	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12193  2re  12194  2cn  12195  0le2  12222  2pos  12223  1p1e2  12240  2p2e4  12250  2times  12251  1p2e3  12258  3p2e5  12266  4p2e6  12268  5p2e7  12271  6p2e8  12274  7p2e9  12276  1lt2  12286  nneo  12552  6p6e12  12657  7p5e12  12660  8p2e10  12663  8p4e12  12665  9p2e11  12670  9p3e12  12671  5t2e10  12683  eluz2b1  12812  x2times  13193  fztp  13475  fz12pr  13476  fztpval  13481  fzo12sn  13643  fzosplitpr  13672  sqval  14016  fac2  14181  faclbnd4lem1  14195  bcp1m1  14222  hashprg  14297  hashgt23el  14326  hashge2el2difr  14383  swrds2  14842  iseralt  15587  binom11  15734  climcndslem1  15751  climcndslem2  15752  bpoly1  15953  bpolydiflem  15956  bpoly3  15960  bpoly4  15961  ege2le3  15992  ef4p  16017  efgt1p2  16018  eirrlem  16108  odd2np1lem  16246  opoe  16269  bitsfzolem  16340  isprm3  16589  prmind2  16591  dvdsnprmd  16596  2mulprm  16599  pockthlem  16812  pockthg  16813  prmunb  16821  prmreclem2  16824  4sqlem19  16870  vdwlem12  16899  prmgaplem8  16965  2expltfac  16999  gsumpr12val  18592  mulg2  18991  psgnunilem2  19402  efgs1b  19643  efgredlemc  19652  lt6abl  19802  abvtrivd  20742  m2detleiblem2  22538  clmvs2  25016  cphipval  25165  pjthlem1  25359  ovolunlem1a  25419  ovolicc1  25439  vitalilem2  25532  itgcnlem  25713  dveflem  25905  coskpi  26454  ang180lem3  26743  tanatan  26851  cosatan  26853  atantayl2  26870  emcllem7  26934  basellem3  27015  basellem5  27017  basellem8  27020  issqf  27068  ppi2  27102  ppi3  27103  cht2  27104  ppieq0  27108  ppiublem2  27136  chpeq0  27141  chtub  27145  chpub  27153  mersenne  27160  perfectlem2  27163  bcp1ctr  27212  bclbnd  27213  bposlem1  27217  bposlem2  27218  bposlem6  27222  lgslem1  27230  lgsval2lem  27240  lgsdir2lem2  27259  lgsdir2lem3  27260  lgsdirprm  27264  lgseisen  27312  m1lgs  27321  rplogsumlem1  27417  rplogsumlem2  27418  dchrisum0flb  27443  dchrisum0re  27446  mulog2sumlem2  27468  pntrmax  27497  pntpbnd2  27520  pntibndlem2  27524  pntlemg  27531  pntlemr  27535  axlowdimlem13  28927  clwlkclwwlklem2a  29970  1wlkdlem1  30109  upgr3v3e3cycl  30152  upgr4cycl4dv4e  30157  numclwlk2lem2f1o  30351  ex-fl  30419  1p1e2apr1  30438  vc2OLD  30540  ipval2  30679  ip2i  30800  hv2times  31033  pjhthlem1  31363  ho2times  31791  stm1addi  32217  staddi  32218  stadd3i  32220  addltmulALT  32418  threehalves  32887  usgrgt2cycl  35166  subfacp1lem1  35215  subfacp1lem5  35220  subfacp1lem6  35221  sin2h  37650  tan2h  37652  poimirlem25  37685  poimirlem27  37687  itg2addnclem3  37713  aks4d1p1p7  42107  facp2  42176  sn-1ne2  42298  remul02  42438  sn-0tie0  42484  3cubeslem3r  42720  pell14qrgapw  42909  rmydioph  43047  rmxdioph  43049  expdiophlem1  43054  expdiophlem2  43055  expdioph  43056  relexp2  43710  stoweidlem14  46052  wallispilem3  46105  wallispi2lem2  46110  fourierswlem  46268  difmodm1lt  47390  perfectALTVlem2  47753  sbgoldbo  47818  nnsum3primes4  47819  nnsum3primesgbe  47823  nnlog2ge0lt1  48598  itcoval2  48696  ackval2  48714  ackval42  48728