Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-7 | Structured version Visualization version GIF version |
Description: Define the number 7. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-7 | ⊢ 7 = (6 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c7 11887 | . 2 class 7 | |
2 | c6 11886 | . . 3 class 6 | |
3 | c1 10727 | . . 3 class 1 | |
4 | caddc 10729 | . . 3 class + | |
5 | 2, 3, 4 | co 7210 | . 2 class (6 + 1) |
6 | 1, 5 | wceq 1543 | 1 wff 7 = (6 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 7nn 11919 7re 11920 7cn 11921 7pos 11938 7m1e6 11959 6p1e7 11975 4p3e7 11981 5p2e7 11983 6p2e8 11986 6lt7 12013 7p7e14 12369 8p7e15 12375 9p7e16 12382 9p8e17 12383 7t7e49 12404 8t7e56 12410 9t7e63 12417 2exp7 16638 7prm 16661 17prm 16667 37prm 16671 317prm 16676 log2ublem2 25827 log2ublem3 25828 bclbnd 26158 bposlem8 26169 lgsdir2lem3 26205 problem4 33336 3cubeslem3r 40210 rmydioph 40537 expdiophlem2 40545 fmtno5 44680 257prm 44684 127prm 44722 7odd 44835 stgoldbwt 44899 |
Copyright terms: Public domain | W3C validator |