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 11685 | . 2 class 6 | |
2 | c5 11684 | . . 3 class 5 | |
3 | c1 10527 | . . 3 class 1 | |
4 | caddc 10529 | . . 3 class + | |
5 | 2, 3, 4 | co 7145 | . 2 class (5 + 1) |
6 | 1, 5 | wceq 1528 | 1 wff 6 = (5 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 6nn 11715 6re 11716 6cn 11717 6pos 11736 6m1e5 11757 5p1e6 11773 3p3e6 11778 4p2e6 11779 5p2e7 11782 5lt6 11807 6p6e12 12161 7p6e13 12165 8p6e14 12171 8p8e16 12173 9p6e15 12178 9p7e16 12179 6t6e36 12195 7t6e42 12200 8t6e48 12206 9t6e54 12213 lt6abl 18946 ppiublem1 25706 ppiublem2 25707 ppiub 25708 bposlem8 25795 lgsdir2lem3 25831 2lgsoddprmlem3d 25917 rmydioph 39491 expdiophlem2 39499 stgoldbwt 43788 sbgoldbm 43796 |
Copyright terms: Public domain | W3C validator |