Definition df-8 9369

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 9361	. 2 class 8
2		c7 9360	. . 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  9389  8pos  9407  8m1e7  9429  7p1e8  9444  4p4e8  9450  5p3e8  9452  6p2e8  9454  7p2e9  9456  8nn  9472  7lt8  9495  8p8e16  9862  9p8e17  9869  9p9e18  9870  8t8e64  9897  9t8e72  9904  log2ublog2  16086