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 10952 | . 2 class 7 | |
2 | c6 10951 | . . 3 class 6 | |
3 | c1 9816 | . . 3 class 1 | |
4 | caddc 9818 | . . 3 class + | |
5 | 2, 3, 4 | co 6549 | . 2 class (6 + 1) |
6 | 1, 5 | wceq 1475 | 1 wff 7 = (6 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 7re 10980 7pos 10997 7m1e6 11018 6p1e7 11033 4p3e7 11040 5p2e7 11042 6p2e8 11046 7nn 11067 6lt7 11086 7p7e14 11485 8p7e15 11493 9p7e16 11501 9p8e17 11502 7t7e49 11529 8t7e56 11537 9t7e63 11544 7prm 15655 17prm 15662 37prm 15666 317prm 15671 log2ublem2 24474 log2ublem3 24475 bclbnd 24805 bposlem8 24816 lgsdir2lem3 24852 2lgslem3d 24924 problem4 30816 rmydioph 36599 expdiophlem2 36607 fmtno5 40007 257prm 40011 2exp7 40052 127prm 40053 7odd 40159 stgoldbwt 40198 |
Copyright terms: Public domain | W3C validator |