| 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 12325 | . 2 class 6 | |
| 2 | c5 12324 | . . 3 class 5 | |
| 3 | c1 11156 | . . 3 class 1 | |
| 4 | caddc 11158 | . . 3 class + | |
| 5 | 2, 3, 4 | co 7431 | . 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 12355 6re 12356 6cn 12357 6pos 12376 6m1e5 12397 5p1e6 12413 3p3e6 12418 4p2e6 12419 5p2e7 12422 5lt6 12447 6p6e12 12807 7p6e13 12811 8p6e14 12817 8p8e16 12819 9p6e15 12824 9p7e16 12825 6t6e36 12841 7t6e42 12846 8t6e48 12852 9t6e54 12859 lt6abl 19913 ppiublem1 27246 ppiublem2 27247 ppiub 27248 bposlem8 27335 lgsdir2lem3 27371 2lgsoddprmlem3d 27457 aks4d1p1p5 42076 rmydioph 43026 expdiophlem2 43034 ceil5half3 47342 stgoldbwt 47763 sbgoldbm 47771 |
| Copyright terms: Public domain | W3C validator |