Definition df-2 9202

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 9194	. 2 class 2
2		c1 8033	. . 3 class 1
3		caddc 8035	. . 3 class +
4	2, 2, 3	co 6018	. 2 class ( 1 + 1 )
5	1, 4	wceq 1397	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9213  0le2  9233  2pos  9234  1p1e2  9260  2p2e4  9270  2times  9271  3p2e5  9285  4p2e6  9287  5p2e7  9290  6p2e8  9293  7p2e9  9295  2nn  9305  1lt2  9313  nneoor  9582  6p6e12  9684  7p5e12  9687  8p2e10  9690  8p4e12  9692  9p2e11  9697  9p3e12  9698  5t2e10  9710  eluz2b1  9835  nn01to3  9851  fztp  10313  fzprval  10317  fztpval  10318  fzo12sn  10463  fzosplitpr  10480  rebtwn2zlemstep  10513  rebtwn2z  10515  sqval  10860  fac2  10994  bcp1m1  11028  hashprg  11073  binom11  12065  ege2le3  12250  ef4p  12273  efgt1p2  12274  eirraplem  12356  odd2np1lem  12451  opoe  12474  bitsfzolem  12533  ncoprmgcdne1b  12679  isprm3  12708  prmind2  12710  dvdsnprmd  12715  prmgt1  12722  pockthlem  12947  pockthg  12948  prmunb  12953  4sqlem19  13000  2expltfac  13030  gsumpr12val  13501  mulg2  13736  dveflem  15469  coskpi  15591  mersenne  15740  perfectlem2  15743  lgslem1  15748  lgsval2lem  15758  lgsdir2lem2  15777  lgsdir2lem3  15778  lgsdirprm  15782  lgseisen  15822  m1lgs  15833  ex-fl  16368