df-9 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-9		Structured version Visualization version GIF version

Definition df-9 11367

Description: Define the number 9. (Contributed by NM, 27-May-1999.)

**Assertion**
Ref	Expression
df-9	⊢ 9 = (8 + 1)

**Detailed syntax breakdown of Definition df-9**
Step	Hyp	Ref	Expression
1		c9 11359	. 2 class 9
2		c8 11358	. . 3 class 8
3		c1 10218	. . 3 class 1
4		caddc 10220	. . 3 class +
5	2, 3, 4	co 6870	. 2 class (8 + 1)
6	1, 5	wceq 1637	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9re 11387 9pos 11401 9m1e8 11422 8p1e9 11437 5p4e9 11445 6p3e9 11447 7p2e9 11448 9nn 11465 8lt9 11494 8p2e10 11835 9p9e18 11849 9t9e81 11884 19prm 16032 139prm 16038 log2tlbnd 24882 bposlem8 25226 lgsdir2lem5 25264 2lgsoddprmlem3b 25346 2lgsoddprmlem3d 25348 rmydioph 38076 139prmALT 42080 9gbo 42231 wtgoldbnnsum4prm 42259 bgoldbnnsum3prm 42261