Definition df-2 12302

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 12294	. 2 class 2
2		c1 11100	. . 3 class 1
3		caddc 11102	. . 3 class +
4	2, 2, 3	co 7411	. 2 class (1 + 1)
5	1, 4	wceq 1567	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12313  2re  12314  2cn  12315  0le2OLD  12343  2posOLD  12345  1p1e2  12363  2m1e1  12364  2p2e4  12374  2times  12375  1p2e3  12382  3p2e5  12390  4p2e6  12392  5p2e7  12395  6p2e8  12398  7p2e9  12400  1lt2  12412  nneo  12679  6p6e12  12789  7p5e12  12792  8p2e10  12795  8p4e12  12797  9p2e11  12802  9p3e12  12803  5t2e10  12815  eluz2b1  12942  x2times  13324  fztp  13607  fz12pr  13608  fztpval  13613  fzo12sn  13776  fzosplitpr  13805  sqval  14149  fac2  14314  faclbnd4lem1  14328  bcp1m1  14355  hashprg  14430  hashgt23el  14460  hashge2el2difr  14517  swrds2  14976  iseralt  15735  binom11  15885  climcndslem1  15902  climcndslem2  15903  bpoly1  16104  bpolydiflem  16107  bpoly3  16111  bpoly4  16112  ege2le3  16143  ef4p  16168  efgt1p2  16169  eirrlem  16259  odd2np1lem  16397  opoe  16420  bitsfzolem  16491  isprm3  16740  prmind2  16742  dvdsnprmd  16747  2mulprm  16750  pockthlem  16964  pockthg  16965  prmunb  16973  prmreclem2  16976  4sqlem19  17022  vdwlem12  17051  prmgaplem8  17117  2expltfac  17151  gsumpr12val  18746  mulg2  19148  psgnunilem2  19564  efgs1b  19805  efgredlemc  19814  lt6abl  19964  abvtrivd  20912  m2detleiblem2  22753  clmvs2  25221  cphipval  25370  pjthlem1  25564  ovolunlem1a  25623  ovolicc1  25643  vitalilem2  25736  itgcnlem  25917  dveflem  26106  coskpi  26653  ang180lem3  26941  tanatan  27049  cosatan  27051  atantayl2  27068  emcllem7  27131  basellem3  27212  basellem5  27214  basellem8  27217  issqf  27265  ppi2  27299  ppi3  27300  cht2  27301  ppieq0  27305  ppiublem2  27332  chpeq0  27337  chtub  27341  chpub  27349  mersenne  27356  perfectlem2  27359  bcp1ctr  27408  bclbnd  27409  bposlem1  27413  bposlem2  27414  bposlem6  27418  lgslem1  27426  lgsval2lem  27436  lgsdir2lem2  27455  lgsdir2lem3  27456  lgsdirprm  27460  lgseisen  27508  m1lgs  27517  rplogsumlem1  27613  rplogsumlem2  27614  dchrisum0flb  27639  dchrisum0re  27642  mulog2sumlem2  27664  pntrmax  27693  pntpbnd2  27716  pntibndlem2  27720  pntlemg  27727  pntlemr  27731  axlowdimlem13  29244  clwlkclwwlklem2a  30289  1wlkdlem1  30428  upgr3v3e3cycl  30471  upgr4cycl4dv4e  30476  numclwlk2lem2f1o  30670  ex-fl  30738  1p1e2apr1  30757  vc2OLD  30860  ipval2  30999  ip2i  31120  hv2times  31353  pjhthlem1  31683  ho2times  32111  stm1addi  32537  staddi  32538  stadd3i  32540  addltmulALT  32738  threehalves  33174  usgrgt2cycl  35520  subfacp1lem1  35569  subfacp1lem5  35574  subfacp1lem6  35575  sin2h  38148  tan2h  38150  poimirlem25  38183  poimirlem27  38185  itg2addnclem3  38211  aks4d1p1p7  42730  facp2  42799  sn-1ne2  42921  remul02  43055  sn-0tie0  43114  3cubeslem3r  43309  pell14qrgapw  43494  rmydioph  43632  rmxdioph  43634  expdiophlem1  43639  expdiophlem2  43640  expdioph  43641  relexp2  44294  stoweidlem14  46619  wallispilem3  46672  wallispi2lem2  46677  fourierswlem  46835  difmodm1lt  47990  perfectALTVlem2  48375  sbgoldbo  48440  nnsum3primes4  48441  nnsum3primesgbe  48445  nnlog2ge0lt1  49230  itcoval2  49328  ackval2  49346  ackval42  49360