Definition df-2 9345

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 9337	. 2 class 2
2		c1 8173	. . 3 class 1
3		caddc 8175	. . 3 class +
4	2, 2, 3	co 6078	. 2 class ( 1 + 1 )
5	1, 4	wceq 1402	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9356  0le2  9376  2pos  9377  1p1e2  9403  2p2e4  9413  2times  9414  3p2e5  9428  4p2e6  9430  5p2e7  9433  6p2e8  9436  7p2e9  9438  2nn  9448  1lt2  9456  nneoor  9730  6p6e12  9832  7p5e12  9835  8p2e10  9838  8p4e12  9840  9p2e11  9845  9p3e12  9846  5t2e10  9858  eluz2b1  9983  nn01to3  9999  fztp  10466  fzprval  10470  fztpval  10471  fzo12sn  10616  fzosplitpr  10633  rebtwn2zlemstep  10668  rebtwn2z  10670  sqval  11015  fac2  11150  bcp1m1  11184  hashprg  11230  binom11  12234  ege2le3  12419  ef4p  12442  efgt1p2  12443  eirraplem  12525  odd2np1lem  12620  opoe  12643  bitsfzolem  12702  ncoprmgcdne1b  12848  isprm3  12877  prmind2  12879  dvdsnprmd  12884  prmgt1  12891  pockthlem  13116  pockthg  13117  prmunb  13122  4sqlem19  13169  2expltfac  13199  mulg2  13914  dveflem  15753  coskpi  15875  mersenne  16028  perfectlem2  16031  lgslem1  16036  lgsval2lem  16046  lgsdir2lem2  16065  lgsdir2lem3  16066  lgsdirprm  16070  lgseisen  16110  m1lgs  16121  ex-fl  16656