Definition df-2 9169

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 9161	. 2 class 2
2		c1 8000	. . 3 class 1
3		caddc 8002	. . 3 class +
4	2, 2, 3	co 6001	. 2 class ( 1 + 1 )
5	1, 4	wceq 1395	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9180  0le2  9200  2pos  9201  1p1e2  9227  2p2e4  9237  2times  9238  3p2e5  9252  4p2e6  9254  5p2e7  9257  6p2e8  9260  7p2e9  9262  2nn  9272  1lt2  9280  nneoor  9549  6p6e12  9651  7p5e12  9654  8p2e10  9657  8p4e12  9659  9p2e11  9664  9p3e12  9665  5t2e10  9677  eluz2b1  9796  nn01to3  9812  fztp  10274  fzprval  10278  fztpval  10279  fzo12sn  10423  rebtwn2zlemstep  10472  rebtwn2z  10474  sqval  10819  fac2  10953  bcp1m1  10987  hashprg  11030  binom11  11997  ege2le3  12182  ef4p  12205  efgt1p2  12206  eirraplem  12288  odd2np1lem  12383  opoe  12406  bitsfzolem  12465  ncoprmgcdne1b  12611  isprm3  12640  prmind2  12642  dvdsnprmd  12647  prmgt1  12654  pockthlem  12879  pockthg  12880  prmunb  12885  4sqlem19  12932  2expltfac  12962  gsumpr12val  13433  mulg2  13668  dveflem  15400  coskpi  15522  mersenne  15671  perfectlem2  15674  lgslem1  15679  lgsval2lem  15689  lgsdir2lem2  15708  lgsdir2lem3  15709  lgsdirprm  15713  lgseisen  15753  m1lgs  15764  ex-fl  16089