Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-5 | Structured version Visualization version GIF version |
Description: Define the number 5. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-5 | ⊢ 5 = (4 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c5 11073 | . 2 class 5 | |
2 | c4 11072 | . . 3 class 4 | |
3 | c1 9937 | . . 3 class 1 | |
4 | caddc 9939 | . . 3 class + | |
5 | 2, 3, 4 | co 6650 | . 2 class (4 + 1) |
6 | 1, 5 | wceq 1483 | 1 wff 5 = (4 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 5re 11099 5pos 11118 5m1e4 11139 4p1e5 11154 3p2e5 11160 4p2e6 11162 5p5e10OLD 11168 5nn 11188 4lt5 11200 5p5e10 11596 6p5e11 11600 6p5e11OLD 11601 7p5e12 11607 8p5e13 11615 8p7e15 11617 9p5e14 11623 9p6e15 11624 5t5e25 11639 5t5e25OLD 11640 6t5e30 11644 6t5e30OLD 11645 7t5e35 11651 8t5e40 11657 8t5e40OLD 11658 9t5e45 11666 fldiv4p1lem1div2 12636 ef01bndlem 14914 prm23lt5 15519 5prm 15815 lt6abl 18296 log2ublem3 24675 ppiublem2 24928 bclbnd 25005 bposlem6 25014 bposlem9 25017 lgsdir2lem3 25052 2lgslem3c 25123 2lgsoddprmlem3c 25137 ex-exp 27307 ex-fac 27308 ex-bc 27309 rmydioph 37581 expdiophlem2 37589 stoweidlem13 40230 fmtno5 41469 fmtnofac1 41482 31prm 41512 5odd 41619 sbgoldbo 41675 |
Copyright terms: Public domain | W3C validator |