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

Definition df-4 10621
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 10612 . 2
2 c3 10611 . . 3
3 c1 9514 . . 3
4 caddc 9516 . . 3
52, 3, 4co 6296 . 2
61, 5wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  4re  10637  4pos  10656  2p2e4  10678  3p1e4  10686  3p2e5  10693  4p4e8  10697  5p4e9  10700  6p4e10  10704  4nn  10720  3lt4  10730  halfpm6th  10785  7p4e11  11056  7p7e14  11059  8p4e12  11061  8p6e14  11063  9p4e13  11068  9p5e14  11069  4t4e16  11077  5t4e20  11079  6t4e24  11083  7t4e28  11088  8t4e32  11094  9t4e36  11101  fzo0to42pr  11901  ef4p  13848  ef01bndlem  13919  lt6abl  16897  iblitg  22175  sincosq4sgn  22894  ang180lem2  23142  binom4  23181  quart1lem  23186  log2cnv  23275  log2ub  23280  ppiublem2  23478  ppiub  23479  chtub  23487  bclbnd  23555  bposlem8  23566  lgsdir2lem3  23600  usgraexvlem  24395  ipval2  25617  problem3  29021  4bc2eq6  29112  bpoly3  29820  bpoly4  29821  fsumcube  29822  rmydioph  30956  rmxdioph  30958  expdiophlem2  30964  lt4addmuld  31506  stoweidlem13  31795
  Copyright terms: Public domain W3C validator