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 11077 | . 2 class 9 | |
2 | c8 11076 | . . 3 class 8 | |
3 | c1 9937 | . . 3 class 1 | |
4 | caddc 9939 | . . 3 class + | |
5 | 2, 3, 4 | co 6650 | . 2 class (8 + 1) |
6 | 1, 5 | wceq 1483 | 1 wff 9 = (8 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 9re 11107 9pos 11122 9m1e8 11143 8p1e9 11158 5p4e9 11167 6p3e9 11170 7p2e9 11172 8p2e10OLD 11174 9nn 11192 8lt9 11222 8p2e10 11610 9p9e18 11627 9t9e81 11670 19prm 15825 139prm 15831 log2tlbnd 24672 bposlem8 25016 lgsdir2lem5 25054 2lgsoddprmlem3b 25136 2lgsoddprmlem3d 25138 rmydioph 37581 139prmALT 41511 9gbo 41662 wtgoldbnnsum4prm 41690 bgoldbnnsum3prm 41692 |
Copyright terms: Public domain | W3C validator |