![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-9 | Structured version Visualization version GIF version |
Description: Define the number 9. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-9 | ⊢ 9 = (8 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c9 12307 | . 2 class 9 | |
2 | c8 12306 | . . 3 class 8 | |
3 | c1 11141 | . . 3 class 1 | |
4 | caddc 11143 | . . 3 class + | |
5 | 2, 3, 4 | co 7419 | . 2 class (8 + 1) |
6 | 1, 5 | wceq 1533 | 1 wff 9 = (8 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 9nn 12343 9re 12344 9cn 12345 9pos 12358 9m1e8 12379 8p1e9 12395 5p4e9 12403 6p3e9 12405 7p2e9 12406 8lt9 12444 8p2e10 12790 9p9e18 12804 9t9e81 12839 19prm 17090 139prm 17096 bposlem8 27269 lgsdir2lem5 27307 2lgsoddprmlem3d 27391 aks4d1p1 41679 rmydioph 42577 139prmALT 47073 9gbo 47251 wtgoldbnnsum4prm 47279 bgoldbnnsum3prm 47281 |
Copyright terms: Public domain | W3C validator |