MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-4 Structured version   Visualization version   GIF version

Definition df-4 10958
Description: Define the number 4. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-4 4 = (3 + 1)

Detailed syntax breakdown of Definition df-4
StepHypRef Expression
1 c4 10949 . 2 class 4
2 c3 10948 . . 3 class 3
3 c1 9816 . . 3 class 1
4 caddc 9818 . . 3 class +
52, 3, 4co 6549 . 2 class (3 + 1)
61, 5wceq 1475 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4re  10974  4pos  10993  4m1e3  11015  2p2e4  11021  3p1e4  11030  3p2e5  11037  4p4e8  11041  5p4e9  11044  6p4e10OLD  11048  4nn  11064  3lt4  11074  halfpm6th  11130  6p4e10  11474  7p4e11  11481  7p4e11OLD  11482  7p7e14  11485  8p4e12  11490  8p6e14  11492  9p4e13  11498  9p5e14  11499  4t4e16  11509  5t4e20  11513  5t4e20OLD  11514  6t4e24  11519  7t4e28  11526  8t4e32  11532  9t4e36  11541  fz0to4untppr  12311  fzo0to42pr  12422  4bc2eq6  12978  bpoly3  14628  bpoly4  14629  fsumcube  14630  ef4p  14682  ef01bndlem  14753  lt6abl  18119  cphipval  22850  iblitg  23341  sincosq4sgn  24057  ang180lem2  24340  binom4  24377  quart1lem  24382  log2cnv  24471  ppiublem2  24728  ppiub  24729  chtub  24737  bclbnd  24805  bposlem8  24816  lgsdir2lem3  24852  ipval2  26946  problem3  30815  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  lt4addmuld  38461  stoweidlem13  38906  4even  40156  31wlkdlem1  41326
  Copyright terms: Public domain W3C validator