Definition df-8 9371

Description: Define the number 8. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-8	|- 8 = ( 7 + 1 )

Detailed syntax breakdown of Definition df-8

Step	Hyp	Ref	Expression
1		c8 9363	. 2 class 8
2		c7 9362	. . 3 class 7
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class ( 7 + 1 )
6	1, 5	wceq 1402	1 wff 8 = ( 7 + 1 )

This definition is used by:  8re  9391  8pos  9409  8m1e7  9431  7p1e8  9446  4p4e8  9452  5p3e8  9454  6p2e8  9456  7p2e9  9458  8nn  9476  7lt8  9499  8p8e16  9871  9p8e17  9878  9p9e18  9879  8t8e64  9906  9t8e72  9913  log2ublog2  16143