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

Definition df-4 9686
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 9677 . 2  class  4
2 c3 9676 . . 3  class  3
3 c1 8618 . . 3  class  1
4 caddc 8620 . . 3  class  +
52, 3, 4co 5710 . 2  class  ( 3  +  1 )
61, 5wceq 1619 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  9699  4pos  9712  2p2e4  9721  3p1e4  9727  3p2e5  9734  4p4e8  9738  5p4e9  9741  6p4e10  9745  4nn  9758  3lt4  9768  halfpm6th  9815  7p4e11  10055  7p7e14  10058  8p4e12  10060  8p6e14  10062  9p4e13  10067  9p5e14  10068  4t4e16  10076  5t4e20  10078  6t4e24  10082  7t4e28  10087  8t4e32  10093  9t4e36  10100  ef4p  12267  ef01bndlem  12338  lt6abl  15016  iblitg  18955  sincosq4sgn  19701  ang180lem2  19940  binom4  19978  quart1lem  19983  log2cnv  20072  log2ub  20077  ppiublem2  20274  ppiub  20275  chtub  20283  bclbnd  20351  bposlem8  20362  lgsdir2lem3  20396  ipval2  21110  4bc2eq6  23269  bpoly3  23967  bpoly4  23968  fsumcube  23969  rmydioph  26273  rmxdioph  26275  expdiophlem2  26281  stoweidlem13  26896  stoweidlem34  26917
  Copyright terms: Public domain W3C validator