Definition df-2 12302

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 12294	. 2 class 2
2		c1 11100	. . 3 class 1
3		caddc 11102	. . 3 class +
4	2, 2, 3	co 7410	. 2 class (1 + 1)
5	1, 4	wceq 1568	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12313  2re  12314  2cn  12315  0le2OLD  12343  2posOLD  12345  1p1e2  12363  2m1e1  12364  2p2e4  12374  2times  12375  1p2e3  12382  3p2e5  12390  4p2e6  12392  5p2e7  12395  6p2e8  12398  7p2e9  12400  1lt2  12412  nneo  12679  6p6e12  12789  7p5e12  12792  8p2e10  12795  8p4e12  12797  9p2e11  12802  9p3e12  12803  5t2e10  12815  eluz2b1  12942  x2times  13324  fztp  13607  fz12pr  13608  fztpval  13613  fzo12sn  13776  fzosplitpr  13805  sqval  14149  fac2  14314  faclbnd4lem1  14328  bcp1m1  14355  hashprg  14430  hashgt23el  14460  hashge2el2difr  14517  swrds2  14976  iseralt  15735  binom11  15885  climcndslem1  15902  climcndslem2  15903  bpoly1  16104  bpolydiflem  16107  bpoly3  16111  bpoly4  16112  ege2le3  16143  ef4p  16168  efgt1p2  16169  eirrlem  16259  odd2np1lem  16397  opoe  16420  bitsfzolem  16491  isprm3  16740  prmind2  16742  dvdsnprmd  16747  2mulprm  16750  pockthlem  16964  pockthg  16965  prmunb  16973  prmreclem2  16976  4sqlem19  17022  vdwlem12  17051  prmgaplem8  17117  2expltfac  17151  gsumpr12val  18746  mulg2  19148  psgnunilem2  19564  efgs1b  19805  efgredlemc  19814  lt6abl  19964  abvtrivd  20914  m2detleiblem2  22764  clmvs2  25232  cphipval  25381  pjthlem1  25575  ovolunlem1a  25634  ovolicc1  25654  vitalilem2  25747  itgcnlem  25928  dveflem  26117  coskpi  26664  ang180lem3  26952  tanatan  27060  cosatan  27062  atantayl2  27079  emcllem7  27142  basellem3  27223  basellem5  27225  basellem8  27228  issqf  27276  ppi2  27310  ppi3  27311  cht2  27312  ppieq0  27316  ppiublem2  27343  chpeq0  27348  chtub  27352  chpub  27360  mersenne  27367  perfectlem2  27370  bcp1ctr  27419  bclbnd  27420  bposlem1  27424  bposlem2  27425  bposlem6  27429  lgslem1  27437  lgsval2lem  27447  lgsdir2lem2  27466  lgsdir2lem3  27467  lgsdirprm  27471  lgseisen  27519  m1lgs  27528  rplogsumlem1  27624  rplogsumlem2  27625  dchrisum0flb  27650  dchrisum0re  27653  mulog2sumlem2  27675  pntrmax  27704  pntpbnd2  27727  pntibndlem2  27731  pntlemg  27738  pntlemr  27742  axlowdimlem13  29270  clwlkclwwlklem2a  30315  1wlkdlem1  30454  upgr3v3e3cycl  30497  upgr4cycl4dv4e  30502  numclwlk2lem2f1o  30696  ex-fl  30764  1p1e2apr1  30783  vc2OLD  30886  ipval2  31025  ip2i  31146  hv2times  31379  pjhthlem1  31709  ho2times  32137  stm1addi  32563  staddi  32564  stadd3i  32566  addltmulALT  32764  threehalves  33200  usgrgt2cycl  35576  subfacp1lem1  35625  subfacp1lem5  35630  subfacp1lem6  35631  sin2h  38205  tan2h  38207  poimirlem25  38240  poimirlem27  38242  itg2addnclem3  38268  aks4d1p1p7  42787  facp2  42856  sn-1ne2  42978  remul02  43112  sn-0tie0  43171  3cubeslem3r  43366  pell14qrgapw  43551  rmydioph  43689  rmxdioph  43691  expdiophlem1  43696  expdiophlem2  43697  expdioph  43698  relexp2  44351  stoweidlem14  46676  wallispilem3  46729  wallispi2lem2  46734  fourierswlem  46892  difmodm1lt  48047  perfectALTVlem2  48432  sbgoldbo  48497  nnsum3primes4  48498  nnsum3primesgbe  48502  nnlog2ge0lt1  49291  itcoval2  49389  ackval2  49407  ackval42  49421