Definition df-2 12209

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 12201	. 2 class 2
2		c1 11028	. . 3 class 1
3		caddc 11030	. . 3 class +
4	2, 2, 3	co 7358	. 2 class (1 + 1)
5	1, 4	wceq 1542	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12219  2re  12220  2cn  12221  0le2  12248  2pos  12249  1p1e2  12266  2p2e4  12276  2times  12277  1p2e3  12284  3p2e5  12292  4p2e6  12294  5p2e7  12297  6p2e8  12300  7p2e9  12302  1lt2  12312  nneo  12577  6p6e12  12682  7p5e12  12685  8p2e10  12688  8p4e12  12690  9p2e11  12695  9p3e12  12696  5t2e10  12708  eluz2b1  12833  x2times  13215  fztp  13497  fz12pr  13498  fztpval  13503  fzo12sn  13665  fzosplitpr  13694  sqval  14038  fac2  14203  faclbnd4lem1  14217  bcp1m1  14244  hashprg  14319  hashgt23el  14348  hashge2el2difr  14405  swrds2  14864  iseralt  15609  binom11  15756  climcndslem1  15773  climcndslem2  15774  bpoly1  15975  bpolydiflem  15978  bpoly3  15982  bpoly4  15983  ege2le3  16014  ef4p  16039  efgt1p2  16040  eirrlem  16130  odd2np1lem  16268  opoe  16291  bitsfzolem  16362  isprm3  16611  prmind2  16613  dvdsnprmd  16618  2mulprm  16621  pockthlem  16834  pockthg  16835  prmunb  16843  prmreclem2  16846  4sqlem19  16892  vdwlem12  16921  prmgaplem8  16987  2expltfac  17021  gsumpr12val  18615  mulg2  19017  psgnunilem2  19428  efgs1b  19669  efgredlemc  19678  lt6abl  19828  abvtrivd  20767  m2detleiblem2  22571  clmvs2  25039  cphipval  25188  pjthlem1  25382  ovolunlem1a  25441  ovolicc1  25461  vitalilem2  25554  itgcnlem  25735  dveflem  25924  coskpi  26472  ang180lem3  26761  tanatan  26869  cosatan  26871  atantayl2  26888  emcllem7  26952  basellem3  27033  basellem5  27035  basellem8  27038  issqf  27086  ppi2  27120  ppi3  27121  cht2  27122  ppieq0  27126  ppiublem2  27154  chpeq0  27159  chtub  27163  chpub  27171  mersenne  27178  perfectlem2  27181  bcp1ctr  27230  bclbnd  27231  bposlem1  27235  bposlem2  27236  bposlem6  27240  lgslem1  27248  lgsval2lem  27258  lgsdir2lem2  27277  lgsdir2lem3  27278  lgsdirprm  27282  lgseisen  27330  m1lgs  27339  rplogsumlem1  27435  rplogsumlem2  27436  dchrisum0flb  27461  dchrisum0re  27464  mulog2sumlem2  27486  pntrmax  27515  pntpbnd2  27538  pntibndlem2  27542  pntlemg  27549  pntlemr  27553  axlowdimlem13  29011  clwlkclwwlklem2a  30057  1wlkdlem1  30196  upgr3v3e3cycl  30239  upgr4cycl4dv4e  30244  numclwlk2lem2f1o  30438  ex-fl  30506  1p1e2apr1  30525  vc2OLD  30628  ipval2  30767  ip2i  30888  hv2times  31121  pjhthlem1  31451  ho2times  31879  stm1addi  32305  staddi  32306  stadd3i  32308  addltmulALT  32506  threehalves  32979  usgrgt2cycl  35318  subfacp1lem1  35367  subfacp1lem5  35372  subfacp1lem6  35373  sin2h  37922  tan2h  37924  poimirlem25  37957  poimirlem27  37959  itg2addnclem3  37985  aks4d1p1p7  42505  facp2  42574  sn-1ne2  42696  remul02  42836  sn-0tie0  42895  3cubeslem3r  43118  pell14qrgapw  43307  rmydioph  43445  rmxdioph  43447  expdiophlem1  43452  expdiophlem2  43453  expdioph  43454  relexp2  44107  stoweidlem14  46446  wallispilem3  46499  wallispi2lem2  46504  fourierswlem  46662  difmodm1lt  47793  perfectALTVlem2  48156  sbgoldbo  48221  nnsum3primes4  48222  nnsum3primesgbe  48226  nnlog2ge0lt1  49000  itcoval2  49098  ackval2  49116  ackval42  49130