Definition df-2 12191

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 12183	. 2 class 2
2		c1 11010	. . 3 class 1
3		caddc 11012	. . 3 class +
4	2, 2, 3	co 7349	. 2 class (1 + 1)
5	1, 4	wceq 1540	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12201  2re  12202  2cn  12203  0le2  12230  2pos  12231  1p1e2  12248  2p2e4  12258  2times  12259  1p2e3  12266  3p2e5  12274  4p2e6  12276  5p2e7  12279  6p2e8  12282  7p2e9  12284  1lt2  12294  nneo  12560  6p6e12  12665  7p5e12  12668  8p2e10  12671  8p4e12  12673  9p2e11  12678  9p3e12  12679  5t2e10  12691  eluz2b1  12820  x2times  13201  fztp  13483  fz12pr  13484  fztpval  13489  fzo12sn  13651  fzosplitpr  13679  sqval  14021  fac2  14186  faclbnd4lem1  14200  bcp1m1  14227  hashprg  14302  hashgt23el  14331  hashge2el2difr  14388  swrds2  14847  iseralt  15592  binom11  15739  climcndslem1  15756  climcndslem2  15757  bpoly1  15958  bpolydiflem  15961  bpoly3  15965  bpoly4  15966  ege2le3  15997  ef4p  16022  efgt1p2  16023  eirrlem  16113  odd2np1lem  16251  opoe  16274  bitsfzolem  16345  isprm3  16594  prmind2  16596  dvdsnprmd  16601  2mulprm  16604  pockthlem  16817  pockthg  16818  prmunb  16826  prmreclem2  16829  4sqlem19  16875  vdwlem12  16904  prmgaplem8  16970  2expltfac  17004  gsumpr12val  18563  mulg2  18962  psgnunilem2  19374  efgs1b  19615  efgredlemc  19624  lt6abl  19774  abvtrivd  20717  m2detleiblem2  22513  clmvs2  24992  cphipval  25141  pjthlem1  25335  ovolunlem1a  25395  ovolicc1  25415  vitalilem2  25508  itgcnlem  25689  dveflem  25881  coskpi  26430  ang180lem3  26719  tanatan  26827  cosatan  26829  atantayl2  26846  emcllem7  26910  basellem3  26991  basellem5  26993  basellem8  26996  issqf  27044  ppi2  27078  ppi3  27079  cht2  27080  ppieq0  27084  ppiublem2  27112  chpeq0  27117  chtub  27121  chpub  27129  mersenne  27136  perfectlem2  27139  bcp1ctr  27188  bclbnd  27189  bposlem1  27193  bposlem2  27194  bposlem6  27198  lgslem1  27206  lgsval2lem  27216  lgsdir2lem2  27235  lgsdir2lem3  27236  lgsdirprm  27240  lgseisen  27288  m1lgs  27297  rplogsumlem1  27393  rplogsumlem2  27394  dchrisum0flb  27419  dchrisum0re  27422  mulog2sumlem2  27444  pntrmax  27473  pntpbnd2  27496  pntibndlem2  27500  pntlemg  27507  pntlemr  27511  axlowdimlem13  28903  clwlkclwwlklem2a  29946  1wlkdlem1  30085  upgr3v3e3cycl  30128  upgr4cycl4dv4e  30133  numclwlk2lem2f1o  30327  ex-fl  30395  1p1e2apr1  30414  vc2OLD  30516  ipval2  30655  ip2i  30776  hv2times  31009  pjhthlem1  31339  ho2times  31767  stm1addi  32193  staddi  32194  stadd3i  32196  addltmulALT  32394  threehalves  32864  usgrgt2cycl  35123  subfacp1lem1  35172  subfacp1lem5  35177  subfacp1lem6  35178  sin2h  37610  tan2h  37612  poimirlem25  37645  poimirlem27  37647  itg2addnclem3  37673  aks4d1p1p7  42067  facp2  42136  sn-1ne2  42258  remul02  42398  sn-0tie0  42444  3cubeslem3r  42680  pell14qrgapw  42869  rmydioph  43007  rmxdioph  43009  expdiophlem1  43014  expdiophlem2  43015  expdioph  43016  relexp2  43670  stoweidlem14  46015  wallispilem3  46068  wallispi2lem2  46073  fourierswlem  46231  difmodm1lt  47363  perfectALTVlem2  47726  sbgoldbo  47791  nnsum3primes4  47792  nnsum3primesgbe  47796  nnlog2ge0lt1  48571  itcoval2  48669  ackval2  48687  ackval42  48701