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 10928
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 10919 . 2 class 4
2 c3 10918 . . 3 class 3
3 c1 9793 . . 3 class 1
4 caddc 9795 . . 3 class +
52, 3, 4co 6527 . 2 class (3 + 1)
61, 5wceq 1474 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4re  10944  4pos  10963  4m1e3  10985  2p2e4  10991  3p1e4  11000  3p2e5  11007  4p4e8  11011  5p4e9  11014  6p4e10OLD  11018  4nn  11034  3lt4  11044  halfpm6th  11100  6p4e10  11430  7p4e11  11437  7p4e11OLD  11438  7p7e14  11441  8p4e12  11446  8p6e14  11448  9p4e13  11454  9p5e14  11455  4t4e16  11465  5t4e20  11469  5t4e20OLD  11470  6t4e24  11475  7t4e28  11482  8t4e32  11488  9t4e36  11497  fz0to4untppr  12266  fzo0to42pr  12377  4bc2eq6  12933  bpoly3  14574  bpoly4  14575  fsumcube  14576  ef4p  14628  ef01bndlem  14699  lt6abl  18065  iblitg  23258  sincosq4sgn  23974  ang180lem2  24257  binom4  24294  quart1lem  24299  log2cnv  24388  ppiublem2  24645  ppiub  24646  chtub  24654  bclbnd  24722  bposlem8  24733  lgsdir2lem3  24769  ipval2  26747  problem3  30621  rmydioph  36395  rmxdioph  36397  expdiophlem2  36403  lt4addmuld  38257  stoweidlem13  38703  4even  39954  31wlkdlem1  41321
  Copyright terms: Public domain W3C validator