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 11688 | . 2 class 9 | |
2 | c8 11687 | . . 3 class 8 | |
3 | c1 10527 | . . 3 class 1 | |
4 | caddc 10529 | . . 3 class + | |
5 | 2, 3, 4 | co 7145 | . 2 class (8 + 1) |
6 | 1, 5 | wceq 1528 | 1 wff 9 = (8 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 9nn 11724 9re 11725 9cn 11726 9pos 11739 9m1e8 11760 8p1e9 11776 5p4e9 11784 6p3e9 11786 7p2e9 11787 8lt9 11825 8p2e10 12167 9p9e18 12181 9t9e81 12216 19prm 16441 139prm 16447 bposlem8 25795 lgsdir2lem5 25833 2lgsoddprmlem3d 25917 rmydioph 39491 139prmALT 43606 9gbo 43786 wtgoldbnnsum4prm 43814 bgoldbnnsum3prm 43816 |
Copyright terms: Public domain | W3C validator |