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 12231

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 12223	. 2 class 8
2		c7 12222	. . 3 class 7
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 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 12257 8re 12258 8cn 12259 8pos 12274 8m1e7 12290 7p1e8 12306 4p4e8 12312 5p3e8 12314 6p2e8 12316 7p2e9 12318 7lt8 12349 8p8e16 12711 9p8e17 12718 9p9e18 12719 8t8e64 12746 9t8e72 12753 log2ub 26835 3cubeslem3r 42648 rmydioph 42976