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 11025
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 11016 . 2 class 4
2 c3 11015 . . 3 class 3
3 c1 9881 . . 3 class 1
4 caddc 9883 . . 3 class +
52, 3, 4co 6604 . 2 class (3 + 1)
61, 5wceq 1480 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4re  11041  4pos  11060  4m1e3  11082  2p2e4  11088  3p1e4  11097  3p2e5  11104  4p4e8  11108  5p4e9  11111  6p4e10OLD  11115  4nn  11131  3lt4  11141  halfpm6th  11197  6p4e10  11542  7p4e11  11549  7p4e11OLD  11550  7p7e14  11553  8p4e12  11558  8p6e14  11560  9p4e13  11566  9p5e14  11567  4t4e16  11577  5t4e20  11581  5t4e20OLD  11582  6t4e24  11587  7t4e28  11594  8t4e32  11600  9t4e36  11609  fz0to4untppr  12383  fzo0to42pr  12496  4bc2eq6  13056  bpoly3  14714  bpoly4  14715  fsumcube  14716  ef4p  14768  ef01bndlem  14839  lt6abl  18217  cphipval  22950  iblitg  23441  sincosq4sgn  24157  ang180lem2  24440  binom4  24477  quart1lem  24482  log2cnv  24571  ppiublem2  24828  ppiub  24829  chtub  24837  bclbnd  24905  bposlem8  24916  lgsdir2lem3  24952  3wlkdlem1  26885  ipval2  27408  problem3  31266  rmydioph  37058  rmxdioph  37060  expdiophlem2  37066  lt4addmuld  38981  stoweidlem13  39534  4even  40914
  Copyright terms: Public domain W3C validator