![]() |
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 12276 | . 2 class 6 | |
2 | c5 12275 | . . 3 class 5 | |
3 | c1 11115 | . . 3 class 1 | |
4 | caddc 11117 | . . 3 class + | |
5 | 2, 3, 4 | co 7412 | . 2 class (5 + 1) |
6 | 1, 5 | wceq 1540 | 1 wff 6 = (5 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 6nn 12306 6re 12307 6cn 12308 6pos 12327 6m1e5 12348 5p1e6 12364 3p3e6 12369 4p2e6 12370 5p2e7 12373 5lt6 12398 6p6e12 12756 7p6e13 12760 8p6e14 12766 8p8e16 12768 9p6e15 12773 9p7e16 12774 6t6e36 12790 7t6e42 12795 8t6e48 12801 9t6e54 12808 lt6abl 19805 ppiublem1 26942 ppiublem2 26943 ppiub 26944 bposlem8 27031 lgsdir2lem3 27067 2lgsoddprmlem3d 27153 aks4d1p1p5 41247 rmydioph 42056 expdiophlem2 42064 stgoldbwt 46743 sbgoldbm 46751 |
Copyright terms: Public domain | W3C validator |