Definition df-2 9261

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 9253	. 2 class 2
2		c1 8093	. . 3 class 1
3		caddc 8095	. . 3 class +
4	2, 2, 3	co 6028	. 2 class ( 1 + 1 )
5	1, 4	wceq 1398	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9272  0le2  9292  2pos  9293  1p1e2  9319  2p2e4  9329  2times  9330  3p2e5  9344  4p2e6  9346  5p2e7  9349  6p2e8  9352  7p2e9  9354  2nn  9364  1lt2  9372  nneoor  9643  6p6e12  9745  7p5e12  9748  8p2e10  9751  8p4e12  9753  9p2e11  9758  9p3e12  9759  5t2e10  9771  eluz2b1  9896  nn01to3  9912  fztp  10375  fzprval  10379  fztpval  10380  fzo12sn  10525  fzosplitpr  10542  rebtwn2zlemstep  10575  rebtwn2z  10577  sqval  10922  fac2  11056  bcp1m1  11090  hashprg  11135  binom11  12127  ege2le3  12312  ef4p  12335  efgt1p2  12336  eirraplem  12418  odd2np1lem  12513  opoe  12536  bitsfzolem  12595  ncoprmgcdne1b  12741  isprm3  12770  prmind2  12772  dvdsnprmd  12777  prmgt1  12784  pockthlem  13009  pockthg  13010  prmunb  13015  4sqlem19  13062  2expltfac  13092  gsumpr12val  13563  mulg2  13798  dveflem  15537  coskpi  15659  mersenne  15811  perfectlem2  15814  lgslem1  15819  lgsval2lem  15829  lgsdir2lem2  15848  lgsdir2lem3  15849  lgsdirprm  15853  lgseisen  15893  m1lgs  15904  ex-fl  16439