Definition df-2 9177

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 9169	. 2 class 2
2		c1 8008	. . 3 class 1
3		caddc 8010	. . 3 class +
4	2, 2, 3	co 6007	. 2 class ( 1 + 1 )
5	1, 4	wceq 1395	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9188  0le2  9208  2pos  9209  1p1e2  9235  2p2e4  9245  2times  9246  3p2e5  9260  4p2e6  9262  5p2e7  9265  6p2e8  9268  7p2e9  9270  2nn  9280  1lt2  9288  nneoor  9557  6p6e12  9659  7p5e12  9662  8p2e10  9665  8p4e12  9667  9p2e11  9672  9p3e12  9673  5t2e10  9685  eluz2b1  9804  nn01to3  9820  fztp  10282  fzprval  10286  fztpval  10287  fzo12sn  10431  rebtwn2zlemstep  10480  rebtwn2z  10482  sqval  10827  fac2  10961  bcp1m1  10995  hashprg  11038  binom11  12005  ege2le3  12190  ef4p  12213  efgt1p2  12214  eirraplem  12296  odd2np1lem  12391  opoe  12414  bitsfzolem  12473  ncoprmgcdne1b  12619  isprm3  12648  prmind2  12650  dvdsnprmd  12655  prmgt1  12662  pockthlem  12887  pockthg  12888  prmunb  12893  4sqlem19  12940  2expltfac  12970  gsumpr12val  13441  mulg2  13676  dveflem  15408  coskpi  15530  mersenne  15679  perfectlem2  15682  lgslem1  15687  lgsval2lem  15697  lgsdir2lem2  15716  lgsdir2lem3  15717  lgsdirprm  15721  lgseisen  15761  m1lgs  15772  ex-fl  16113