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 11085

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 11076	. 2 class 8
2		c7 11075	. . 3 class 7
3		c1 9937	. . 3 class 1
4		caddc 9939	. . 3 class +
5	2, 3, 4	co 6650	. 2 class (7 + 1)
6	1, 5	wceq 1483	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8re 11105 8pos 11121 8m1e7 11142 7p1e8 11157 4p4e8 11164 5p3e8 11166 6p2e8 11169 7p2e9 11172 8nn 11191 7lt8 11215 8p8e16 11618 9p8e17 11626 9p9e18 11627 8t8e64 11662 9t8e72 11669 log2ub 24676 lgsdir2lem1 25050 lgsdir2lem3 25052 rmydioph 37581