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 12380

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 12372	. 2 class 8
2		c7 12371	. . 3 class 7
3		c1 11172	. . 3 class 1
4		caddc 11174	. . 3 class +
5	2, 3, 4	co 7408	. 2 class (7 + 1)
6	1, 5	wceq 1570	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is used by: 8nn 12407 8re 12408 8cn 12409 8m1e7 12444 7p1e8 12460 4p4e8 12466 5p3e8 12468 6p2e8 12470 7p2e9 12472 7lt8 12506 8p8e16 12874 9p8e17 12881 9p9e18 12882 8t8e64 12909 9t8e72 12916 log2ub 27240 1p8e9 43235 3cubeslem3r 43636 rmydioph 43959