Definition df-2 12374

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 12366	. 2 class 2
2		c1 11172	. . 3 class 1
3		caddc 11174	. . 3 class +
4	2, 2, 3	co 7408	. 2 class (1 + 1)
5	1, 4	wceq 1570	1 wff 2 = (1 + 1)

This definition is used by:  2nn  12385  2re  12386  2cn  12387  0le2OLD  12415  2posOLD  12417  1p1e2  12435  2m1e1  12436  2p2e4  12446  2times  12447  1p2e3  12454  3p2e5  12462  4p2e6  12464  5p2e7  12467  6p2e8  12470  7p2e9  12472  1lt2  12484  nneo  12752  6p6e12  12862  7p5e12  12865  8p2e10  12868  8p4e12  12870  9p2e11  12875  9p3e12  12876  5t2e10  12888  eluz2b1  13015  x2times  13398  fztp  13682  fz12pr  13683  fztpval  13688  fzo12sn  13851  fzosplitpr  13880  sqval  14225  fac2  14390  faclbnd4lem1  14404  bcp1m1  14431  hashprg  14506  hashgt23el  14536  hashge2el2difr  14593  swrds2  15058  iseralt  15819  binom11  15968  climcndslem1  15985  climcndslem2  15986  bpoly1  16184  bpolydiflem  16187  bpoly3  16191  bpoly4  16192  ege2le3  16223  ef4p  16248  efgt1p2  16249  eirrlem  16339  odd2np1lem  16477  opoe  16500  bitsfzolem  16571  isprm3  16820  prmind2  16822  dvdsnprmd  16827  2mulprm  16830  pockthlem  17044  pockthg  17045  prmunb  17053  prmreclem2  17056  4sqlem19  17102  vdwlem12  17131  prmgaplem8  17197  2expltfac  17231  gsumpr12val  18839  mulg2  19254  psgnunilem2  19670  efgs1b  19911  efgredlemc  19920  lt6abl  20070  abvtrivd  21050  m2detleiblem2  22904  clmvs2  25376  cphipval  25525  pjthlem1  25719  ovolunlem1a  25778  ovolicc1  25798  vitalilem2  25891  itgcnlem  26071  dveflem  26260  coskpi  26814  ang180lem3  27102  tanatan  27210  cosatan  27212  atantayl2  27229  emcllem7  27292  basellem3  27373  basellem5  27375  basellem8  27378  issqf  27426  ppi2  27460  ppi3  27461  cht2  27462  ppieq0  27466  ppiublem2  27493  chpeq0  27498  chtub  27502  chpub  27510  mersenne  27517  perfectlem2  27520  bcp1ctr  27569  bclbnd  27570  bposlem1  27574  bposlem2  27575  bposlem6  27579  lgslem1  27587  lgsval2lem  27597  lgsdir2lem2  27616  lgsdir2lem3  27617  lgsdirprm  27621  lgseisen  27669  m1lgs  27678  rplogsumlem1  27774  rplogsumlem2  27775  dchrisum0flb  27800  dchrisum0re  27803  mulog2sumlem2  27825  pntrmax  27854  pntpbnd2  27877  pntibndlem2  27881  pntlemg  27888  pntlemr  27892  axlowdimlem13  29465  clwlkclwwlklem2a  30522  1wlkdlem1  30661  upgr3v3e3cycl  30714  upgr4cycl4dv4e  30719  numclwlk2lem2f1o  30913  ex-fl  30981  1p1e2apr1  31000  vc2OLD  31103  ipval2  31242  ip2i  31363  hv2times  31596  pjhthlem1  31926  ho2times  32354  stm1addi  32780  staddi  32781  stadd3i  32783  addltmulALT  32981  threehalves  33414  usgrgt2cycl  35830  subfacp1lem1  35865  subfacp1lem5  35870  subfacp1lem6  35871  sin2h  38453  tan2h  38455  poimirlem25  38483  poimirlem27  38485  itg2addnclem3  38511  aks4d1p1p7  43044  facp2  43113  sn-1ne2  43250  remul02  43384  sn-0tie0  43443  3cubeslem3r  43636  pell14qrgapw  43821  rmydioph  43959  rmxdioph  43961  expdiophlem1  43966  expdiophlem2  43967  expdioph  43968  relexp2  44621  stoweidlem14  46946  wallispilem3  46999  wallispi2lem2  47004  fourierswlem  47162  difmodm1lt  48357  perfectALTVlem2  48742  sbgoldbo  48807  nnsum3primes4  48808  nnsum3primesgbe  48812  nnlog2ge0lt1  49600  itcoval2  49698  ackval2  49716  ackval42  49730