Definition df-2 11941

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 11933	. 2 class 2
2		c1 10778	. . 3 class 1
3		caddc 10780	. . 3 class +
4	2, 2, 3	co 7252	. 2 class (1 + 1)
5	1, 4	wceq 1543	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  11951  2re  11952  2cn  11953  0le2  11980  2pos  11981  1p1e2  12003  2p2e4  12013  2times  12014  1p2e3  12021  3p2e5  12029  4p2e6  12031  5p2e7  12034  6p2e8  12037  7p2e9  12039  1lt2  12049  nneo  12309  6p6e12  12415  7p5e12  12418  8p2e10  12421  8p4e12  12423  9p2e11  12428  9p3e12  12429  5t2e10  12441  eluz2b1  12563  x2times  12937  fztp  13216  fz12pr  13217  fztpval  13222  fzo12sn  13373  fzosplitpr  13399  sqval  13738  fac2  13896  faclbnd4lem1  13910  bcp1m1  13937  hashprg  14013  hashgt23el  14042  hashge2el2difr  14098  swrds2  14556  iseralt  15299  binom11  15447  climcndslem1  15464  climcndslem2  15465  bpoly1  15664  bpolydiflem  15667  bpoly3  15671  bpoly4  15672  ege2le3  15702  ef4p  15725  efgt1p2  15726  eirrlem  15816  odd2np1lem  15952  opoe  15975  bitsfzolem  16044  isprm3  16291  prmind2  16293  dvdsnprmd  16298  2mulprm  16301  pockthlem  16509  pockthg  16510  prmunb  16518  prmreclem2  16521  4sqlem19  16567  vdwlem12  16596  prmgaplem8  16662  decexp2  16679  2expltfac  16697  gsumpr12val  18263  mulg2  18603  psgnunilem2  18993  efgs1b  19232  efgredlemc  19241  lt6abl  19386  abvtrivd  19990  m2detleiblem2  21660  clmvs2  24138  cphipval  24287  pjthlem1  24481  ovolunlem1a  24540  ovolicc1  24560  vitalilem2  24653  itgcnlem  24834  dveflem  25023  coskpi  25559  ang180lem3  25841  tanatan  25949  cosatan  25951  atantayl2  25968  emcllem7  26031  basellem3  26112  basellem5  26114  basellem8  26117  issqf  26165  ppi2  26199  ppi3  26200  cht2  26201  ppieq0  26205  ppiublem2  26231  chpeq0  26236  chtub  26240  chpub  26248  mersenne  26255  perfectlem2  26258  bcp1ctr  26307  bclbnd  26308  bposlem1  26312  bposlem2  26313  bposlem6  26317  lgslem1  26325  lgsval2lem  26335  lgsdir2lem2  26354  lgsdir2lem3  26355  lgsdirprm  26359  lgseisen  26407  m1lgs  26416  rplogsumlem1  26512  rplogsumlem2  26513  dchrisum0flb  26538  dchrisum0re  26541  mulog2sumlem2  26563  pntrmax  26592  pntpbnd2  26615  pntibndlem2  26619  pntlemg  26626  pntlemr  26630  axlowdimlem13  27200  clwlkclwwlklem2a  28238  1wlkdlem1  28377  upgr3v3e3cycl  28420  upgr4cycl4dv4e  28425  numclwlk2lem2f1o  28619  ex-fl  28687  1p1e2apr1  28706  vc2OLD  28806  ipval2  28945  ip2i  29066  hv2times  29299  pjhthlem1  29629  ho2times  30057  stm1addi  30483  staddi  30484  stadd3i  30486  addltmulALT  30684  threehalves  31066  usgrgt2cycl  32967  subfacp1lem1  33016  subfacp1lem5  33021  subfacp1lem6  33022  sin2h  35673  tan2h  35675  poimirlem25  35708  poimirlem27  35710  itg2addnclem3  35736  aks4d1p1p7  39988  facp2  39999  fac2xp3  40060  sn-1ne2  40188  remul02  40281  sn-0tie0  40314  3cubeslem3r  40397  pell14qrgapw  40586  rmydioph  40724  rmxdioph  40726  expdiophlem1  40731  expdiophlem2  40732  expdioph  40733  relexp2  41147  stoweidlem14  43418  wallispilem3  43471  wallispi2lem2  43476  fourierswlem  43634  perfectALTVlem2  45035  sbgoldbo  45100  nnsum3primes4  45101  nnsum3primesgbe  45105  difmodm1lt  45729  nnlog2ge0lt1  45773  itcoval2  45871  ackval2  45889  ackval42  45903