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 10759
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 10750 . 2 class 4
2 c3 10749 . . 3 class 3
3 c1 9625 . . 3 class 1
4 caddc 9627 . . 3 class +
52, 3, 4co 6363 . 2 class (3 + 1)
61, 5wceq 1468 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4re  10775  4pos  10794  4m1e3  10816  2p2e4  10817  3p1e4  10825  3p2e5  10832  4p4e8  10836  5p4e9  10839  6p4e10  10843  4nn  10859  3lt4  10869  halfpm6th  10924  7p4e11  11193  7p7e14  11196  8p4e12  11198  8p6e14  11200  9p4e13  11205  9p5e14  11206  4t4e16  11214  5t4e20  11216  6t4e24  11220  7t4e28  11225  8t4e32  11231  9t4e36  11238  fzo0to42pr  12104  4bc2eq6  12628  bpoly3  14271  bpoly4  14272  fsumcube  14273  ef4p  14327  ef01bndlem  14398  lt6abl  17690  iblitg  22887  sincosq4sgn  23617  ang180lem2  23900  binom4  23937  quart1lem  23942  log2cnv  24031  log2ub  24036  ppiublem2  24292  ppiub  24293  chtub  24301  bclbnd  24369  bposlem8  24380  lgsdir2lem3  24414  usgraexmplvtxlem  25283  ipval2  26506  problem3  30451  rmydioph  36109  rmxdioph  36111  expdiophlem2  36117  lt4addmuld  37901  stoweidlem13  38309  4even  39356  31wlkdlem1  40726
  Copyright terms: Public domain W3C validator