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 12278

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 12270	. 2 class 8
2		c7 12269	. . 3 class 7
3		c1 11108	. . 3 class 1
4		caddc 11110	. . 3 class +
5	2, 3, 4	co 7406	. 2 class (7 + 1)
6	1, 5	wceq 1542	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12304 8re 12305 8cn 12306 8pos 12321 8m1e7 12342 7p1e8 12358 4p4e8 12364 5p3e8 12366 6p2e8 12368 7p2e9 12370 7lt8 12401 8p8e16 12760 9p8e17 12767 9p9e18 12768 8t8e64 12795 9t8e72 12802 log2ub 26444 3cubeslem3r 41411 rmydioph 41739