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 11707

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 11699	. 2 class 8
2		c7 11698	. . 3 class 7
3		c1 10538	. . 3 class 1
4		caddc 10540	. . 3 class +
5	2, 3, 4	co 7156	. 2 class (7 + 1)
6	1, 5	wceq 1537	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 11733 8re 11734 8cn 11735 8pos 11750 8m1e7 11771 7p1e8 11787 4p4e8 11793 5p3e8 11795 6p2e8 11797 7p2e9 11799 7lt8 11830 8p8e16 12185 9p8e17 12192 9p9e18 12193 8t8e64 12220 9t8e72 12227 log2ub 25527 3cubeslem3r 39333 rmydioph 39660