| 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 12323 | . 2 class 4 | |
| 2 | c3 12322 | . . 3 class 3 | |
| 3 | c1 11156 | . . 3 class 1 | |
| 4 | caddc 11158 | . . 3 class + | |
| 5 | 2, 3, 4 | co 7431 | . 2 class (3 + 1) |
| 6 | 1, 5 | wceq 1540 | 1 wff 4 = (3 + 1) |
| Colors of variables: wff setvar class |
| This definition is referenced by: 4nn 12349 4re 12350 4cn 12351 4pos 12373 4m1e3 12395 2p2e4 12401 3p1e4 12411 3p2e5 12417 4p4e8 12421 5p4e9 12424 3lt4 12440 halfpm6th 12487 6p4e10 12805 7p4e11 12809 7p7e14 12812 8p4e12 12815 8p6e14 12817 9p4e13 12822 9p5e14 12823 4t4e16 12832 5t4e20 12835 6t4e24 12839 7t4e28 12844 8t4e32 12850 9t4e36 12857 fz0to4untppr 13670 4bc2eq6 14368 bpoly3 16094 bpoly4 16095 fsumcube 16096 ef4p 16149 ef01bndlem 16220 ge2nprmge4 16738 lt6abl 19913 cphipval 25277 sincosq4sgn 26543 binom4 26893 quart1lem 26898 log2cnv 26987 ppiublem2 27247 ppiub 27248 chtub 27256 bclbnd 27324 bposlem8 27335 lgsdir2lem3 27371 3wlkdlem1 30178 ipval2 30726 problem3 35672 aks4d1p1p7 42075 rmydioph 43026 rmxdioph 43028 expdiophlem2 43034 lt4addmuld 45318 stoweidlem13 46028 m1modnep2mod 47354 4even 47696 sbgoldbo 47774 ackval40 48614 ackval41a 48615 ackval42 48617 |
| Copyright terms: Public domain | W3C validator |