Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-4 | Structured version Visualization version GIF version |
Description: Define the number 4. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-4 | ⊢ 4 = (3 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c4 11695 | . 2 class 4 | |
2 | c3 11694 | . . 3 class 3 | |
3 | c1 10538 | . . 3 class 1 | |
4 | caddc 10540 | . . 3 class + | |
5 | 2, 3, 4 | co 7156 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1537 | 1 wff 4 = (3 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 4nn 11721 4re 11722 4cn 11723 4pos 11745 4m1e3 11767 2p2e4 11773 3p1e4 11783 3p2e5 11789 4p4e8 11793 5p4e9 11796 3lt4 11812 halfpm6th 11859 6p4e10 12171 7p4e11 12175 7p7e14 12178 8p4e12 12181 8p6e14 12183 9p4e13 12188 9p5e14 12189 4t4e16 12198 5t4e20 12201 6t4e24 12205 7t4e28 12210 8t4e32 12216 9t4e36 12223 fz0to4untppr 13011 4bc2eq6 13690 bpoly3 15412 bpoly4 15413 fsumcube 15414 ef4p 15466 ef01bndlem 15537 ge2nprmge4 16045 lt6abl 19015 cphipval 23846 sincosq4sgn 25087 binom4 25428 quart1lem 25433 log2cnv 25522 ppiublem2 25779 ppiub 25780 chtub 25788 bclbnd 25856 bposlem8 25867 lgsdir2lem3 25903 3wlkdlem1 27938 ipval2 28484 problem3 32910 rmydioph 39660 rmxdioph 39662 expdiophlem2 39668 lt4addmuld 41622 stoweidlem13 42347 4even 43923 sbgoldbo 44001 |
Copyright terms: Public domain | W3C validator |