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

Definition df-4 9822
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 9813 . 2  class  4
2 c3 9812 . . 3  class  3
3 c1 8754 . . 3  class  1
4 caddc 8756 . . 3  class  +
52, 3, 4co 5874 . 2  class  ( 3  +  1 )
61, 5wceq 1632 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  9835  4pos  9848  2p2e4  9858  3p1e4  9864  3p2e5  9871  4p4e8  9875  5p4e9  9878  6p4e10  9882  4nn  9895  3lt4  9905  halfpm6th  9952  7p4e11  10192  7p7e14  10195  8p4e12  10197  8p6e14  10199  9p4e13  10204  9p5e14  10205  4t4e16  10213  5t4e20  10215  6t4e24  10219  7t4e28  10224  8t4e32  10230  9t4e36  10237  ef4p  12409  ef01bndlem  12480  lt6abl  15197  iblitg  19139  sincosq4sgn  19885  ang180lem2  20124  binom4  20162  quart1lem  20167  log2cnv  20256  log2ub  20261  ppiublem2  20458  ppiub  20459  chtub  20467  bclbnd  20535  bposlem8  20546  lgsdir2lem3  20580  ipval2  21296  4bc2eq6  24114  bpoly3  24865  bpoly4  24866  fsumcube  24867  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  stoweidlem13  27865  stoweidlem34  27886  fzo0to42pr  28211  usgraexvlem  28261
  Copyright terms: Public domain W3C validator