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 10954 | . 2 class 9 | |
2 | c8 10953 | . . 3 class 8 | |
3 | c1 9816 | . . 3 class 1 | |
4 | caddc 9818 | . . 3 class + | |
5 | 2, 3, 4 | co 6549 | . 2 class (8 + 1) |
6 | 1, 5 | wceq 1475 | 1 wff 9 = (8 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 9re 10984 9pos 10999 9m1e8 11020 8p1e9 11035 5p4e9 11044 6p3e9 11047 7p2e9 11049 8p2e10OLD 11051 9nn 11069 8lt9 11099 8p2e10 11486 9p9e18 11503 9t9e81 11546 19prm 15663 139prm 15669 log2tlbnd 24472 bposlem8 24816 lgsdir2lem5 24854 2lgsoddprmlem3b 24936 2lgsoddprmlem3d 24938 rmydioph 36599 139prmALT 40049 9gboa 40196 wtgoldbnnsum4prm 40218 bgoldbnnsum3prm 40220 |
Copyright terms: Public domain | W3C validator |