Definition df-8 9378

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 9370	. 2 class 8
2		c7 9369	. . 3 class 7
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class ( 7 + 1 )
6	1, 5	wceq 1402	1 wff 8 = ( 7 + 1 )

This definition is used by:  8re  9398  8pos  9416  8m1e7  9438  7p1e8  9453  4p4e8  9459  5p3e8  9461  6p2e8  9463  7p2e9  9465  8nn  9483  7lt8  9506  8p8e16  9878  9p8e17  9885  9p9e18  9886  8t8e64  9913  9t8e72  9920  log2ublog2  16224