df-8 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-8		Structured version Visualization version GIF version

Definition df-8 12315

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 12307	. 2 class 8
2		c7 12306	. . 3 class 7
3		c1 11107	. . 3 class 1
4		caddc 11109	. . 3 class +
5	2, 3, 4	co 7412	. 2 class (7 + 1)
6	1, 5	wceq 1569	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is used by: 8nn 12342 8re 12343 8cn 12344 8m1e7 12379 7p1e8 12395 4p4e8 12401 5p3e8 12403 6p2e8 12405 7p2e9 12407 7lt8 12441 8p8e16 12808 9p8e17 12815 9p9e18 12816 8t8e64 12843 9t8e72 12850 log2ub 27125 3cubeslem3r 43446 rmydioph 43769