Definition df-2 12206

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 12198	. 2 class 2
2		c1 11025	. . 3 class 1
3		caddc 11027	. . 3 class +
4	2, 2, 3	co 7356	. 2 class (1 + 1)
5	1, 4	wceq 1541	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12216  2re  12217  2cn  12218  0le2  12245  2pos  12246  1p1e2  12263  2p2e4  12273  2times  12274  1p2e3  12281  3p2e5  12289  4p2e6  12291  5p2e7  12294  6p2e8  12297  7p2e9  12299  1lt2  12309  nneo  12574  6p6e12  12679  7p5e12  12682  8p2e10  12685  8p4e12  12687  9p2e11  12692  9p3e12  12693  5t2e10  12705  eluz2b1  12830  x2times  13212  fztp  13494  fz12pr  13495  fztpval  13500  fzo12sn  13662  fzosplitpr  13691  sqval  14035  fac2  14200  faclbnd4lem1  14214  bcp1m1  14241  hashprg  14316  hashgt23el  14345  hashge2el2difr  14402  swrds2  14861  iseralt  15606  binom11  15753  climcndslem1  15770  climcndslem2  15771  bpoly1  15972  bpolydiflem  15975  bpoly3  15979  bpoly4  15980  ege2le3  16011  ef4p  16036  efgt1p2  16037  eirrlem  16127  odd2np1lem  16265  opoe  16288  bitsfzolem  16359  isprm3  16608  prmind2  16610  dvdsnprmd  16615  2mulprm  16618  pockthlem  16831  pockthg  16832  prmunb  16840  prmreclem2  16843  4sqlem19  16889  vdwlem12  16918  prmgaplem8  16984  2expltfac  17018  gsumpr12val  18612  mulg2  19011  psgnunilem2  19422  efgs1b  19663  efgredlemc  19672  lt6abl  19822  abvtrivd  20763  m2detleiblem2  22570  clmvs2  25048  cphipval  25197  pjthlem1  25391  ovolunlem1a  25451  ovolicc1  25471  vitalilem2  25564  itgcnlem  25745  dveflem  25937  coskpi  26486  ang180lem3  26775  tanatan  26883  cosatan  26885  atantayl2  26902  emcllem7  26966  basellem3  27047  basellem5  27049  basellem8  27052  issqf  27100  ppi2  27134  ppi3  27135  cht2  27136  ppieq0  27140  ppiublem2  27168  chpeq0  27173  chtub  27177  chpub  27185  mersenne  27192  perfectlem2  27195  bcp1ctr  27244  bclbnd  27245  bposlem1  27249  bposlem2  27250  bposlem6  27254  lgslem1  27262  lgsval2lem  27272  lgsdir2lem2  27291  lgsdir2lem3  27292  lgsdirprm  27296  lgseisen  27344  m1lgs  27353  rplogsumlem1  27449  rplogsumlem2  27450  dchrisum0flb  27475  dchrisum0re  27478  mulog2sumlem2  27500  pntrmax  27529  pntpbnd2  27552  pntibndlem2  27556  pntlemg  27563  pntlemr  27567  axlowdimlem13  28976  clwlkclwwlklem2a  30022  1wlkdlem1  30161  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  numclwlk2lem2f1o  30403  ex-fl  30471  1p1e2apr1  30490  vc2OLD  30592  ipval2  30731  ip2i  30852  hv2times  31085  pjhthlem1  31415  ho2times  31843  stm1addi  32269  staddi  32270  stadd3i  32272  addltmulALT  32470  threehalves  32945  usgrgt2cycl  35273  subfacp1lem1  35322  subfacp1lem5  35327  subfacp1lem6  35328  sin2h  37750  tan2h  37752  poimirlem25  37785  poimirlem27  37787  itg2addnclem3  37813  aks4d1p1p7  42267  facp2  42336  sn-1ne2  42462  remul02  42602  sn-0tie0  42648  3cubeslem3r  42871  pell14qrgapw  43060  rmydioph  43198  rmxdioph  43200  expdiophlem1  43205  expdiophlem2  43206  expdioph  43207  relexp2  43860  stoweidlem14  46200  wallispilem3  46253  wallispi2lem2  46258  fourierswlem  46416  difmodm1lt  47547  perfectALTVlem2  47910  sbgoldbo  47975  nnsum3primes4  47976  nnsum3primesgbe  47980  nnlog2ge0lt1  48754  itcoval2  48852  ackval2  48870  ackval42  48884