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 10840
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 10831 . 2 class 4
2 c3 10830 . . 3 class 3
3 c1 9696 . . 3 class 1
4 caddc 9698 . . 3 class +
52, 3, 4co 6431 . 2 class (3 + 1)
61, 5wceq 1474 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4re  10856  4pos  10875  4m1e3  10897  2p2e4  10903  3p1e4  10912  3p2e5  10919  4p4e8  10923  5p4e9  10926  6p4e10OLD  10930  4nn  10946  3lt4  10956  halfpm6th  11012  6p4e10  11342  7p4e11  11349  7p4e11OLD  11350  7p7e14  11353  8p4e12  11358  8p6e14  11360  9p4e13  11366  9p5e14  11367  4t4e16  11377  5t4e20  11381  5t4e20OLD  11382  6t4e24  11387  7t4e28  11394  8t4e32  11400  9t4e36  11409  fz0to4untppr  12183  fzo0to42pr  12294  4bc2eq6  12850  bpoly3  14501  bpoly4  14502  fsumcube  14503  ef4p  14555  ef01bndlem  14626  lt6abl  18030  iblitg  23220  sincosq4sgn  23948  ang180lem2  24231  binom4  24268  quart1lem  24273  log2cnv  24362  ppiublem2  24621  ppiub  24622  chtub  24630  bclbnd  24698  bposlem8  24709  lgsdir2lem3  24745  ipval2  26723  problem3  30662  rmydioph  36493  rmxdioph  36495  expdiophlem2  36501  lt4addmuld  38363  stoweidlem13  38813  4even  40068  31wlkdlem1  41435
  Copyright terms: Public domain W3C validator