![]() |
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 11684 | . 2 class 6 | |
2 | c5 11683 | . . 3 class 5 | |
3 | c1 10527 | . . 3 class 1 | |
4 | caddc 10529 | . . 3 class + | |
5 | 2, 3, 4 | co 7135 | . 2 class (5 + 1) |
6 | 1, 5 | wceq 1538 | 1 wff 6 = (5 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 6nn 11714 6re 11715 6cn 11716 6pos 11735 6m1e5 11756 5p1e6 11772 3p3e6 11777 4p2e6 11778 5p2e7 11781 5lt6 11806 6p6e12 12160 7p6e13 12164 8p6e14 12170 8p8e16 12172 9p6e15 12177 9p7e16 12178 6t6e36 12194 7t6e42 12199 8t6e48 12205 9t6e54 12212 lt6abl 19008 ppiublem1 25786 ppiublem2 25787 ppiub 25788 bposlem8 25875 lgsdir2lem3 25911 2lgsoddprmlem3d 25997 rmydioph 39955 expdiophlem2 39963 stgoldbwt 44294 sbgoldbm 44302 |
Copyright terms: Public domain | W3C validator |