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

Definition df-4 9806
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 9797 . 2  class  4
2 c3 9796 . . 3  class  3
3 c1 8738 . . 3  class  1
4 caddc 8740 . . 3  class  +
52, 3, 4co 5858 . 2  class  ( 3  +  1 )
61, 5wceq 1623 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  9819  4pos  9832  2p2e4  9842  3p1e4  9848  3p2e5  9855  4p4e8  9859  5p4e9  9862  6p4e10  9866  4nn  9879  3lt4  9889  halfpm6th  9936  7p4e11  10176  7p7e14  10179  8p4e12  10181  8p6e14  10183  9p4e13  10188  9p5e14  10189  4t4e16  10197  5t4e20  10199  6t4e24  10203  7t4e28  10208  8t4e32  10214  9t4e36  10221  ef4p  12393  ef01bndlem  12464  lt6abl  15181  iblitg  19123  sincosq4sgn  19869  ang180lem2  20108  binom4  20146  quart1lem  20151  log2cnv  20240  log2ub  20245  ppiublem2  20442  ppiub  20443  chtub  20451  bclbnd  20519  bposlem8  20530  lgsdir2lem3  20564  ipval2  21280  4bc2eq6  24099  bpoly3  24793  bpoly4  24794  fsumcube  24795  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115  stoweidlem13  27762  stoweidlem34  27783  usgraexvlem  28127
  Copyright terms: Public domain W3C validator