Definition df-2 9180

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 9172	. 2 class 2
2		c1 8011	. . 3 class 1
3		caddc 8013	. . 3 class +
4	2, 2, 3	co 6007	. 2 class ( 1 + 1 )
5	1, 4	wceq 1395	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9191  0le2  9211  2pos  9212  1p1e2  9238  2p2e4  9248  2times  9249  3p2e5  9263  4p2e6  9265  5p2e7  9268  6p2e8  9271  7p2e9  9273  2nn  9283  1lt2  9291  nneoor  9560  6p6e12  9662  7p5e12  9665  8p2e10  9668  8p4e12  9670  9p2e11  9675  9p3e12  9676  5t2e10  9688  eluz2b1  9808  nn01to3  9824  fztp  10286  fzprval  10290  fztpval  10291  fzo12sn  10435  rebtwn2zlemstep  10484  rebtwn2z  10486  sqval  10831  fac2  10965  bcp1m1  10999  hashprg  11043  binom11  12013  ege2le3  12198  ef4p  12221  efgt1p2  12222  eirraplem  12304  odd2np1lem  12399  opoe  12422  bitsfzolem  12481  ncoprmgcdne1b  12627  isprm3  12656  prmind2  12658  dvdsnprmd  12663  prmgt1  12670  pockthlem  12895  pockthg  12896  prmunb  12901  4sqlem19  12948  2expltfac  12978  gsumpr12val  13449  mulg2  13684  dveflem  15416  coskpi  15538  mersenne  15687  perfectlem2  15690  lgslem1  15695  lgsval2lem  15705  lgsdir2lem2  15724  lgsdir2lem3  15725  lgsdirprm  15729  lgseisen  15769  m1lgs  15780  ex-fl  16172