Definition df-2 9363

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 9355	. 2 class 2
2		c1 8180	. . 3 class 1
3		caddc 8182	. . 3 class +
4	2, 2, 3	co 6085	. 2 class ( 1 + 1 )
5	1, 4	wceq 1402	1 wff 2 = ( 1 + 1 )

This definition is used by:  2re  9374  0le2  9394  2pos  9395  1p1e2  9421  2p2e4  9431  2times  9432  3p2e5  9446  4p2e6  9448  5p2e7  9451  6p2e8  9454  7p2e9  9456  2nn  9466  1lt2  9474  nneoor  9748  6p6e12  9850  7p5e12  9853  8p2e10  9856  8p4e12  9858  9p2e11  9863  9p3e12  9864  5t2e10  9876  eluz2b1  10001  nn01to3  10017  fztp  10485  fzprval  10489  fztpval  10490  fzo12sn  10635  fzosplitpr  10652  rebtwn2zlemstep  10687  rebtwn2z  10689  sqval  11034  fac2  11169  bcp1m1  11203  hashprg  11249  binom11  12253  ege2le3  12438  ef4p  12461  efgt1p2  12462  eirraplem  12544  odd2np1lem  12639  opoe  12662  bitsfzolem  12721  ncoprmgcdne1b  12867  isprm3  12896  prmind2  12898  dvdsnprmd  12903  prmgt1  12910  pockthlem  13135  pockthg  13136  prmunb  13141  4sqlem19  13188  2expltfac  13218  mulg2  13934  dveflem  15827  coskpi  15949  mersenne  16111  perfectlem2  16114  lgslem1  16119  lgsval2lem  16129  lgsdir2lem2  16148  lgsdir2lem3  16149  lgsdirprm  16153  lgseisen  16193  m1lgs  16204  ex-fl  16739