![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-6 | Structured version Visualization version GIF version |
Description: Define the number 6. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-6 | ⊢ 6 = (5 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c6 11499 | . 2 class 6 | |
2 | c5 11498 | . . 3 class 5 | |
3 | c1 10336 | . . 3 class 1 | |
4 | caddc 10338 | . . 3 class + | |
5 | 2, 3, 4 | co 6976 | . 2 class (5 + 1) |
6 | 1, 5 | wceq 1507 | 1 wff 6 = (5 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 6nn 11532 6re 11533 6cn 11534 6pos 11557 6m1e5 11578 5p1e6 11594 3p3e6 11599 4p2e6 11600 5p2e7 11603 5lt6 11628 6p6e12 11987 7p6e13 11991 8p6e14 11997 8p8e16 11999 9p6e15 12004 9p7e16 12005 6t6e36 12021 7t6e42 12026 8t6e48 12032 9t6e54 12039 lt6abl 18769 ppiublem1 25480 ppiublem2 25481 ppiub 25482 bposlem8 25569 lgsdir2lem3 25605 2lgsoddprmlem3d 25691 rmydioph 39013 expdiophlem2 39021 stgoldbwt 43315 sbgoldbm 43323 |
Copyright terms: Public domain | W3C validator |