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 12336

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 12328	. 2 class 8
2		c7 12327	. . 3 class 7
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7416	. 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 12363 8re 12364 8cn 12365 8m1e7 12400 7p1e8 12416 4p4e8 12422 5p3e8 12424 6p2e8 12426 7p2e9 12428 7lt8 12462 8p8e16 12830 9p8e17 12837 9p9e18 12838 8t8e64 12865 9t8e72 12872 log2ub 27184 1p8e9 43118 3cubeslem3r 43519 rmydioph 43842