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 12255

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 12247	. 2 class 8
2		c7 12246	. . 3 class 7
3		c1 11069	. . 3 class 1
4		caddc 11071	. . 3 class +
5	2, 3, 4	co 7387	. 2 class (7 + 1)
6	1, 5	wceq 1540	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12281 8re 12282 8cn 12283 8pos 12298 8m1e7 12314 7p1e8 12330 4p4e8 12336 5p3e8 12338 6p2e8 12340 7p2e9 12342 7lt8 12373 8p8e16 12735 9p8e17 12742 9p9e18 12743 8t8e64 12770 9t8e72 12777 log2ub 26859 3cubeslem3r 42675 rmydioph 43003