Definition df-2 11701

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 11693	. 2 class 2
2		c1 10538	. . 3 class 1
3		caddc 10540	. . 3 class +
4	2, 2, 3	co 7156	. 2 class (1 + 1)
5	1, 4	wceq 1537	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  11711  2re  11712  2cn  11713  0le2  11740  2pos  11741  1p1e2  11763  2p2e4  11773  2times  11774  1p2e3  11781  3p2e5  11789  4p2e6  11791  5p2e7  11794  6p2e8  11797  7p2e9  11799  1lt2  11809  nneo  12067  6p6e12  12173  7p5e12  12176  8p2e10  12179  8p4e12  12181  9p2e11  12186  9p3e12  12187  5t2e10  12199  eluz2b1  12320  x2times  12693  fztp  12964  fz12pr  12965  fztpval  12970  fzo12sn  13121  fzosplitpr  13147  sqval  13482  fac2  13640  faclbnd4lem1  13654  bcp1m1  13681  hashprg  13757  hashgt23el  13786  hashge2el2difr  13840  swrds2  14302  iseralt  15041  binom11  15187  climcndslem1  15204  climcndslem2  15205  bpoly1  15405  bpolydiflem  15408  bpoly3  15412  bpoly4  15413  ege2le3  15443  ef4p  15466  efgt1p2  15467  eirrlem  15557  odd2np1lem  15689  opoe  15712  bitsfzolem  15783  isprm3  16027  prmind2  16029  dvdsnprmd  16034  2mulprm  16037  pockthlem  16241  pockthg  16242  prmunb  16250  prmreclem2  16253  4sqlem19  16299  vdwlem12  16328  prmgaplem8  16394  decexp2  16411  2expltfac  16426  gsumpr12val  17899  mulg2  18237  psgnunilem2  18623  efgs1b  18862  efgredlemc  18871  lt6abl  19015  abvtrivd  19611  m2detleiblem2  21237  clmvs2  23698  cphipval  23846  pjthlem1  24040  ovolunlem1a  24097  ovolicc1  24117  vitalilem2  24210  itgcnlem  24390  dveflem  24576  coskpi  25108  ang180lem3  25389  tanatan  25497  cosatan  25499  atantayl2  25516  emcllem7  25579  basellem3  25660  basellem5  25662  basellem8  25665  issqf  25713  ppi2  25747  ppi3  25748  cht2  25749  ppieq0  25753  ppiublem2  25779  chpeq0  25784  chtub  25788  chpub  25796  mersenne  25803  perfectlem2  25806  bcp1ctr  25855  bclbnd  25856  bposlem1  25860  bposlem2  25861  bposlem6  25865  lgslem1  25873  lgsval2lem  25883  lgsdir2lem2  25902  lgsdir2lem3  25903  lgsdirprm  25907  lgseisen  25955  m1lgs  25964  rplogsumlem1  26060  rplogsumlem2  26061  dchrisum0flb  26086  dchrisum0re  26089  mulog2sumlem2  26111  pntrmax  26140  pntpbnd2  26163  pntibndlem2  26167  pntlemg  26174  pntlemr  26178  axlowdimlem13  26740  clwlkclwwlklem2a  27776  1wlkdlem1  27916  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  numclwlk2lem2f1o  28158  ex-fl  28226  1p1e2apr1  28245  vc2OLD  28345  ipval2  28484  ip2i  28605  hv2times  28838  pjhthlem1  29168  ho2times  29596  stm1addi  30022  staddi  30023  stadd3i  30025  addltmulALT  30223  threehalves  30591  usgrgt2cycl  32377  subfacp1lem1  32426  subfacp1lem5  32431  subfacp1lem6  32432  sin2h  34897  tan2h  34899  poimirlem25  34932  poimirlem27  34934  itg2addnclem3  34960  fac2xp3  39143  facp2  39144  sn-1ne2  39207  remul02  39284  3cubeslem3r  39333  pell14qrgapw  39522  rmydioph  39660  rmxdioph  39662  expdiophlem1  39667  expdiophlem2  39668  expdioph  39669  relexp2  40071  stoweidlem14  42348  wallispilem3  42401  wallispi2lem2  42406  fourierswlem  42564  perfectALTVlem2  43936  sbgoldbo  44001  nnsum3primes4  44002  nnsum3primesgbe  44006  difmodm1lt  44631  nnlog2ge0lt1  44675