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 11686 | . 2 class 7 | |
2 | c6 11685 | . . 3 class 6 | |
3 | c1 10527 | . . 3 class 1 | |
4 | caddc 10529 | . . 3 class + | |
5 | 2, 3, 4 | co 7145 | . 2 class (6 + 1) |
6 | 1, 5 | wceq 1528 | 1 wff 7 = (6 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 7nn 11718 7re 11719 7cn 11720 7pos 11737 7m1e6 11758 6p1e7 11774 4p3e7 11780 5p2e7 11782 6p2e8 11785 6lt7 11812 7p7e14 12166 8p7e15 12172 9p7e16 12179 9p8e17 12180 7t7e49 12201 8t7e56 12207 9t7e63 12214 7prm 16434 17prm 16440 37prm 16444 317prm 16449 log2ublem2 25453 log2ublem3 25454 bclbnd 25784 bposlem8 25795 lgsdir2lem3 25831 problem4 32809 3cubeslem3r 39164 rmydioph 39491 expdiophlem2 39499 fmtno5 43566 257prm 43570 2exp7 43609 127prm 43610 7odd 43724 stgoldbwt 43788 |
Copyright terms: Public domain | W3C validator |