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

Definition df-4 9801
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 9792 . 2  class  4
2 c3 9791 . . 3  class  3
3 c1 8733 . . 3  class  1
4 caddc 8735 . . 3  class  +
52, 3, 4co 5819 . 2  class  ( 3  +  1 )
61, 5wceq 1624 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  9814  4pos  9827  2p2e4  9837  3p1e4  9843  3p2e5  9850  4p4e8  9854  5p4e9  9857  6p4e10  9861  4nn  9874  3lt4  9884  halfpm6th  9931  7p4e11  10171  7p7e14  10174  8p4e12  10176  8p6e14  10178  9p4e13  10183  9p5e14  10184  4t4e16  10192  5t4e20  10194  6t4e24  10198  7t4e28  10203  8t4e32  10209  9t4e36  10216  ef4p  12387  ef01bndlem  12458  lt6abl  15175  iblitg  19117  sincosq4sgn  19863  ang180lem2  20102  binom4  20140  quart1lem  20145  log2cnv  20234  log2ub  20239  ppiublem2  20436  ppiub  20437  chtub  20445  bclbnd  20513  bposlem8  20524  lgsdir2lem3  20558  ipval2  21272  4bc2eq6  23502  bpoly3  24200  bpoly4  24201  fsumcube  24202  rmydioph  26506  rmxdioph  26508  expdiophlem2  26514  stoweidlem13  27161  stoweidlem34  27182
  Copyright terms: Public domain W3C validator