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 11123

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 11114	. 2 class 8
2		c7 11113	. . 3 class 7
3		c1 9975	. . 3 class 1
4		caddc 9977	. . 3 class +
5	2, 3, 4	co 6690	. 2 class (7 + 1)
6	1, 5	wceq 1523	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8re 11143 8pos 11159 8m1e7 11180 7p1e8 11195 4p4e8 11202 5p3e8 11204 6p2e8 11207 7p2e9 11210 8nn 11229 7lt8 11253 8p8e16 11656 9p8e17 11664 9p9e18 11665 8t8e64 11700 9t8e72 11707 log2ub 24721 lgsdir2lem1 25095 lgsdir2lem3 25097 rmydioph 37898