Definition df-8 12197

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 12189	. 2 class 8
2		c7 12188	. . 3 class 7
3		c1 11010	. . 3 class 1
4		caddc 11012	. . 3 class +
5	2, 3, 4	co 7349	. 2 class (7 + 1)
6	1, 5	wceq 1540	1 wff 8 = (7 + 1)

This definition is referenced by:  8nn  12223  8re  12224  8cn  12225  8pos  12240  8m1e7  12256  7p1e8  12272  4p4e8  12278  5p3e8  12280  6p2e8  12282  7p2e9  12284  7lt8  12315  8p8e16  12677  9p8e17  12684  9p9e18  12685  8t8e64  12712  9t8e72  12719  log2ub  26857  3cubeslem3r  42664  rmydioph  42991