![]() |
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 11496 | . 2 class 9 | |
2 | c8 11495 | . . 3 class 8 | |
3 | c1 10330 | . . 3 class 1 | |
4 | caddc 10332 | . . 3 class + | |
5 | 2, 3, 4 | co 6970 | . 2 class (8 + 1) |
6 | 1, 5 | wceq 1507 | 1 wff 9 = (8 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 9nn 11538 9re 11539 9cn 11540 9pos 11554 9m1e8 11575 8p1e9 11591 5p4e9 11599 6p3e9 11601 7p2e9 11602 8lt9 11640 8p2e10 11987 9p9e18 12001 9t9e81 12036 19prm 16301 139prm 16307 bposlem8 25563 lgsdir2lem5 25601 2lgsoddprmlem3d 25685 rmydioph 39007 139prmALT 43127 9gbo 43307 wtgoldbnnsum4prm 43335 bgoldbnnsum3prm 43337 |
Copyright terms: Public domain | W3C validator |