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 12212

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 12204	. 2 class 8
2		c7 12203	. . 3 class 7
3		c1 11025	. . 3 class 1
4		caddc 11027	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (7 + 1)
6	1, 5	wceq 1541	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12238 8re 12239 8cn 12240 8pos 12255 8m1e7 12271 7p1e8 12287 4p4e8 12293 5p3e8 12295 6p2e8 12297 7p2e9 12299 7lt8 12330 8p8e16 12691 9p8e17 12698 9p9e18 12699 8t8e64 12726 9t8e72 12733 log2ub 26913 3cubeslem3r 42871 rmydioph 43198