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 11506

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 11498	. 2 class 8
2		c7 11497	. . 3 class 7
3		c1 10332	. . 3 class 1
4		caddc 10334	. . 3 class +
5	2, 3, 4	co 6974	. 2 class (7 + 1)
6	1, 5	wceq 1507	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 11537 8re 11538 8cn 11539 8pos 11556 8m1e7 11577 7p1e8 11593 4p4e8 11599 5p3e8 11601 6p2e8 11603 7p2e9 11605 7lt8 11636 8p8e16 11996 9p8e17 12003 9p9e18 12004 8t8e64 12031 9t8e72 12038 log2ub 25223 rmydioph 38985