Definition df-2 9313

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 9305	. 2 class 2
2		c1 8144	. . 3 class 1
3		caddc 8146	. . 3 class +
4	2, 2, 3	co 6058	. 2 class ( 1 + 1 )
5	1, 4	wceq 1398	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9324  0le2  9344  2pos  9345  1p1e2  9371  2p2e4  9381  2times  9382  3p2e5  9396  4p2e6  9398  5p2e7  9401  6p2e8  9404  7p2e9  9406  2nn  9416  1lt2  9424  nneoor  9698  6p6e12  9800  7p5e12  9803  8p2e10  9806  8p4e12  9808  9p2e11  9813  9p3e12  9814  5t2e10  9826  eluz2b1  9951  nn01to3  9967  fztp  10434  fzprval  10438  fztpval  10439  fzo12sn  10584  fzosplitpr  10601  rebtwn2zlemstep  10636  rebtwn2z  10638  sqval  10983  fac2  11118  bcp1m1  11152  hashprg  11198  binom11  12197  ege2le3  12382  ef4p  12405  efgt1p2  12406  eirraplem  12488  odd2np1lem  12583  opoe  12606  bitsfzolem  12665  ncoprmgcdne1b  12811  isprm3  12840  prmind2  12842  dvdsnprmd  12847  prmgt1  12854  pockthlem  13079  pockthg  13080  prmunb  13085  4sqlem19  13132  2expltfac  13162  gsumpr12val  13663  mulg2  13884  dveflem  15717  coskpi  15839  mersenne  15991  perfectlem2  15994  lgslem1  15999  lgsval2lem  16009  lgsdir2lem2  16028  lgsdir2lem3  16029  lgsdirprm  16033  lgseisen  16073  m1lgs  16084  ex-fl  16619