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 10962

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 10953	. 2 class 8
2		c7 10952	. . 3 class 7
3		c1 9816	. . 3 class 1
4		caddc 9818	. . 3 class +
5	2, 3, 4	co 6549	. 2 class (7 + 1)
6	1, 5	wceq 1475	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8re 10982 8pos 10998 8m1e7 11019 7p1e8 11034 4p4e8 11041 5p3e8 11043 6p2e8 11046 7p2e9 11049 8nn 11068 7lt8 11092 8p8e16 11494 9p8e17 11502 9p9e18 11503 8t8e64 11538 9t8e72 11545 log2ub 24476 lgsdir2lem1 24850 lgsdir2lem3 24852 rmydioph 36599