Definition df-2 11079

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 11070	. 2 class 2
2		c1 9937	. . 3 class 1
3		caddc 9939	. . 3 class +
4	2, 2, 3	co 6650	. 2 class ( 1 + 1 )
5	1, 4	wceq 1483	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  11090  0le2  11111  2pos  11112  1p1e2  11134  2p2e4  11144  2times  11145  3p2e5  11160  4p2e6  11162  5p2e7  11165  6p2e8  11169  7p2e9  11172  8p2e10OLD  11174  2nn  11185  1lt2  11194  nneo  11461  6p6e12  11602  7p5e12  11607  8p2e10  11610  8p4e12  11614  9p2e11  11619  9p2e11OLD  11620  9p3e12  11621  5t2e10  11634  eluz2b1  11759  x2times  12129  fztp  12397  fzprval  12401  fztpval  12402  fzo12sn  12551  fzosplitpr  12577  sqval  12922  fac2  13066  faclbnd4lem1  13080  bcp1m1  13107  hashprg  13182  hashprgOLD  13183  hashge2el2difr  13263  swrds2  13685  iseralt  14415  binom11  14564  climcndslem1  14581  climcndslem2  14582  bpoly1  14782  bpolydiflem  14785  bpoly3  14789  bpoly4  14790  ege2le3  14820  ef4p  14843  efgt1p2  14844  eirrlem  14932  odd2np1lem  15064  opoe  15087  bitsfzolem  15156  isprm3  15396  prmind2  15398  dvdsnprmd  15403  prmgt1  15409  pockthlem  15609  pockthg  15610  prmunb  15618  prmreclem2  15621  4sqlem19  15667  vdwlem12  15696  prmgaplem8  15762  decexp2  15779  2expltfac  15799  gsumpr12val  17282  mulg2  17550  psgnunilem2  17915  efgs1b  18149  efgredlemc  18158  lt6abl  18296  abvtrivd  18840  m2detleiblem2  20434  clmvs2  22894  cphipval  23042  pjthlem1  23208  ovolunlem1a  23264  ovolicc1  23284  vitalilem2  23378  itgcnlem  23556  dveflem  23742  coskpi  24272  ang180lem3  24541  tanatan  24646  cosatan  24648  atantayl2  24665  emcllem7  24728  basellem3  24809  basellem5  24811  basellem8  24814  issqf  24862  ppi2  24896  ppi3  24897  cht2  24898  ppieq0  24902  ppiublem2  24928  chpeq0  24933  chtub  24937  chpub  24945  mersenne  24952  perfectlem2  24955  bcp1ctr  25004  bclbnd  25005  bposlem1  25009  bposlem2  25010  bposlem6  25014  lgslem1  25022  lgsval2lem  25032  lgsdir2lem2  25051  lgsdir2lem3  25052  lgsdirprm  25056  lgseisen  25104  m1lgs  25113  rplogsumlem1  25173  rplogsumlem2  25174  dchrisum0flb  25199  dchrisum0re  25202  mulog2sumlem2  25224  pntrmax  25253  pntpbnd2  25276  pntibndlem2  25280  pntlemg  25287  pntlemr  25291  axlowdimlem4  25825  axlowdimlem13  25834  clwlkclwwlklem2a  26899  1wlkdlem1  26997  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  numclwlk2lem2f1o  27238  ex-fl  27304  1p1e2apr1  27322  vc2OLD  27423  ipval2  27562  ip2i  27683  hv2times  27918  pjhthlem1  28250  ho2times  28678  stm1addi  29104  staddi  29105  stadd3i  29107  addltmulALT  29305  threehalves  29623  subfacp1lem1  31161  subfacp1lem5  31166  subfacp1lem6  31167  sin2h  33399  tan2h  33401  poimirlem25  33434  poimirlem27  33436  itg2addnclem3  33463  pell14qrgapw  37440  rmydioph  37581  rmxdioph  37583  expdiophlem1  37588  expdiophlem2  37589  expdioph  37590  relexp2  37969  stoweidlem14  40231  wallispilem3  40284  wallispi2lem2  40289  fourierswlem  40447  perfectALTVlem2  41631  sbgoldbo  41675  nnsum3primes4  41676  nnsum3primesgbe  41680  difmodm1lt  42317  nnlog2ge0lt1  42360