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 11700 | . 2 class 9 | |
2 | c8 11699 | . . 3 class 8 | |
3 | c1 10538 | . . 3 class 1 | |
4 | caddc 10540 | . . 3 class + | |
5 | 2, 3, 4 | co 7156 | . 2 class (8 + 1) |
6 | 1, 5 | wceq 1537 | 1 wff 9 = (8 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 9nn 11736 9re 11737 9cn 11738 9pos 11751 9m1e8 11772 8p1e9 11788 5p4e9 11796 6p3e9 11798 7p2e9 11799 8lt9 11837 8p2e10 12179 9p9e18 12193 9t9e81 12228 19prm 16451 139prm 16457 bposlem8 25867 lgsdir2lem5 25905 2lgsoddprmlem3d 25989 rmydioph 39660 139prmALT 43808 9gbo 43988 wtgoldbnnsum4prm 44016 bgoldbnnsum3prm 44018 |
Copyright terms: Public domain | W3C validator |