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 11074 | . 2 class 6 | |
2 | c5 11073 | . . 3 class 5 | |
3 | c1 9937 | . . 3 class 1 | |
4 | caddc 9939 | . . 3 class + | |
5 | 2, 3, 4 | co 6650 | . 2 class (5 + 1) |
6 | 1, 5 | wceq 1483 | 1 wff 6 = (5 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 6re 11101 6pos 11119 6m1e5 11140 5p1e6 11155 3p3e6 11161 4p2e6 11162 5p2e7 11165 6nn 11189 5lt6 11204 6p6e12 11602 7p6e13 11608 8p6e14 11616 8p8e16 11618 9p6e15 11624 9p7e16 11625 6t6e36 11646 6t6e36OLD 11647 7t6e42 11652 8t6e48 11659 8t6e48OLD 11660 9t6e54 11667 lt6abl 18296 ppiublem1 24927 ppiublem2 24928 ppiub 24929 bposlem8 25016 lgsdir2lem3 25052 2lgsoddprmlem3d 25138 rmydioph 37581 expdiophlem2 37589 stgoldbwt 41664 sbgoldbm 41672 |
Copyright terms: Public domain | W3C validator |