MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-4 Unicode version

Definition df-4 10111
Description: Define the number 4. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-4

Detailed syntax breakdown of Definition df-4
StepHypRef Expression
1 c4 10102 . 2
2 c3 10101 . . 3
3 c1 9042 . . 3
4 caddc 9044 . . 3
52, 3, 4co 6129 . 2
61, 5wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  4re  10124  4pos  10137  2p2e4  10149  3p1e4  10155  3p2e5  10162  4p4e8  10166  5p4e9  10169  6p4e10  10173  4nn  10186  3lt4  10196  halfpm6th  10243  7p4e11  10485  7p7e14  10488  8p4e12  10490  8p6e14  10492  9p4e13  10497  9p5e14  10498  4t4e16  10506  5t4e20  10508  6t4e24  10512  7t4e28  10517  8t4e32  10523  9t4e36  10530  fzo0to42pr  11237  ef4p  12765  ef01bndlem  12836  lt6abl  15555  iblitg  19709  sincosq4sgn  20460  ang180lem2  20703  binom4  20741  quart1lem  20746  log2cnv  20835  log2ub  20840  ppiublem2  21038  ppiub  21039  chtub  21047  bclbnd  21115  bposlem8  21126  lgsdir2lem3  21160  usgraexvlem  21465  ipval2  22254  4bc2eq6  25308  bpoly3  26208  bpoly4  26209  fsumcube  26210  rmydioph  27264  rmxdioph  27266  expdiophlem2  27272  stoweidlem13  27916
  Copyright terms: Public domain W3C validator