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 11244
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 11235 . 2 class 4
2 c3 11234 . . 3 class 3
3 c1 10100 . . 3 class 1
4 caddc 10102 . . 3 class +
52, 3, 4co 6801 . 2 class (3 + 1)
61, 5wceq 1620 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4re  11260  4pos  11279  4m1e3  11301  2p2e4  11307  3p1e4  11316  3p2e5  11323  4p4e8  11327  5p4e9  11330  6p4e10OLD  11334  4nn  11350  3lt4  11360  halfpm6th  11416  6p4e10  11761  7p4e11  11768  7p4e11OLD  11769  7p7e14  11772  8p4e12  11777  8p6e14  11779  9p4e13  11785  9p5e14  11786  4t4e16  11796  5t4e20  11800  5t4e20OLD  11801  6t4e24  11806  7t4e28  11813  8t4e32  11819  9t4e36  11828  fz0to4untppr  12607  fzo0to42pr  12720  4bc2eq6  13281  bpoly3  14959  bpoly4  14960  fsumcube  14961  ef4p  15013  ef01bndlem  15084  lt6abl  18467  cphipval  23213  iblitg  23705  sincosq4sgn  24423  ang180lem2  24710  binom4  24747  quart1lem  24752  log2cnv  24841  ppiublem2  25098  ppiub  25099  chtub  25107  bclbnd  25175  bposlem8  25186  lgsdir2lem3  25222  3wlkdlem1  27282  ipval2  27842  problem3  31839  rmydioph  38052  rmxdioph  38054  expdiophlem2  38060  lt4addmuld  39988  stoweidlem13  40702  4even  42097  sbgoldbo  42154
  Copyright terms: Public domain W3C validator