Definition df-2 11688

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 11680	. 2 class 2
2		c1 10527	. . 3 class 1
3		caddc 10529	. . 3 class +
4	2, 2, 3	co 7135	. 2 class (1 + 1)
5	1, 4	wceq 1538	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  11698  2re  11699  2cn  11700  0le2  11727  2pos  11728  1p1e2  11750  2p2e4  11760  2times  11761  1p2e3  11768  3p2e5  11776  4p2e6  11778  5p2e7  11781  6p2e8  11784  7p2e9  11786  1lt2  11796  nneo  12054  6p6e12  12160  7p5e12  12163  8p2e10  12166  8p4e12  12168  9p2e11  12173  9p3e12  12174  5t2e10  12186  eluz2b1  12307  x2times  12680  fztp  12958  fz12pr  12959  fztpval  12964  fzo12sn  13115  fzosplitpr  13141  sqval  13477  fac2  13635  faclbnd4lem1  13649  bcp1m1  13676  hashprg  13752  hashgt23el  13781  hashge2el2difr  13835  swrds2  14293  iseralt  15033  binom11  15179  climcndslem1  15196  climcndslem2  15197  bpoly1  15397  bpolydiflem  15400  bpoly3  15404  bpoly4  15405  ege2le3  15435  ef4p  15458  efgt1p2  15459  eirrlem  15549  odd2np1lem  15681  opoe  15704  bitsfzolem  15773  isprm3  16017  prmind2  16019  dvdsnprmd  16024  2mulprm  16027  pockthlem  16231  pockthg  16232  prmunb  16240  prmreclem2  16243  4sqlem19  16289  vdwlem12  16318  prmgaplem8  16384  decexp2  16401  2expltfac  16418  gsumpr12val  17891  mulg2  18229  psgnunilem2  18615  efgs1b  18854  efgredlemc  18863  lt6abl  19008  abvtrivd  19604  m2detleiblem2  21233  clmvs2  23699  cphipval  23847  pjthlem1  24041  ovolunlem1a  24100  ovolicc1  24120  vitalilem2  24213  itgcnlem  24393  dveflem  24582  coskpi  25115  ang180lem3  25397  tanatan  25505  cosatan  25507  atantayl2  25524  emcllem7  25587  basellem3  25668  basellem5  25670  basellem8  25673  issqf  25721  ppi2  25755  ppi3  25756  cht2  25757  ppieq0  25761  ppiublem2  25787  chpeq0  25792  chtub  25796  chpub  25804  mersenne  25811  perfectlem2  25814  bcp1ctr  25863  bclbnd  25864  bposlem1  25868  bposlem2  25869  bposlem6  25873  lgslem1  25881  lgsval2lem  25891  lgsdir2lem2  25910  lgsdir2lem3  25911  lgsdirprm  25915  lgseisen  25963  m1lgs  25972  rplogsumlem1  26068  rplogsumlem2  26069  dchrisum0flb  26094  dchrisum0re  26097  mulog2sumlem2  26119  pntrmax  26148  pntpbnd2  26171  pntibndlem2  26175  pntlemg  26182  pntlemr  26186  axlowdimlem13  26748  clwlkclwwlklem2a  27783  1wlkdlem1  27922  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  numclwlk2lem2f1o  28164  ex-fl  28232  1p1e2apr1  28251  vc2OLD  28351  ipval2  28490  ip2i  28611  hv2times  28844  pjhthlem1  29174  ho2times  29602  stm1addi  30028  staddi  30029  stadd3i  30031  addltmulALT  30229  threehalves  30617  usgrgt2cycl  32490  subfacp1lem1  32539  subfacp1lem5  32544  subfacp1lem6  32545  sin2h  35047  tan2h  35049  poimirlem25  35082  poimirlem27  35084  itg2addnclem3  35110  facp2  39347  fac2xp3  39385  sn-1ne2  39466  remul02  39543  sn-0tie0  39576  3cubeslem3r  39628  pell14qrgapw  39817  rmydioph  39955  rmxdioph  39957  expdiophlem1  39962  expdiophlem2  39963  expdioph  39964  relexp2  40378  stoweidlem14  42656  wallispilem3  42709  wallispi2lem2  42714  fourierswlem  42872  perfectALTVlem2  44240  sbgoldbo  44305  nnsum3primes4  44306  nnsum3primesgbe  44310  difmodm1lt  44936  nnlog2ge0lt1  44980  itcoval2  45078  ackval2  45096  ackval42  45110