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 11696 | . 2 class 5 | |
2 | c4 11695 | . . 3 class 4 | |
3 | c1 10538 | . . 3 class 1 | |
4 | caddc 10540 | . . 3 class + | |
5 | 2, 3, 4 | co 7156 | . 2 class (4 + 1) |
6 | 1, 5 | wceq 1537 | 1 wff 5 = (4 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 5nn 11724 5re 11725 5cn 11726 5pos 11747 5m1e4 11768 4p1e5 11784 3p2e5 11789 4p2e6 11791 4lt5 11815 5p5e10 12170 6p5e11 12172 7p5e12 12176 8p5e13 12182 8p7e15 12184 9p5e14 12189 9p6e15 12190 5t5e25 12202 6t5e30 12206 7t5e35 12211 8t5e40 12217 9t5e45 12224 fldiv4p1lem1div2 13206 ef01bndlem 15537 prm23lt5 16151 5prm 16442 lt6abl 19015 log2ublem3 25526 ppiublem2 25779 bclbnd 25856 bposlem6 25865 bposlem9 25868 lgsdir2lem3 25903 2lgslem3c 25974 2lgsoddprmlem3c 25988 ex-exp 28229 ex-fac 28230 ex-bc 28231 rmydioph 39660 expdiophlem2 39668 stoweidlem13 42347 fmtno5 43768 fmtnofac1 43781 31prm 43809 5odd 43924 sbgoldbo 44001 |
Copyright terms: Public domain | W3C validator |