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

Definition df-4 9774
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 9765 . 2  class  4
2 c3 9764 . . 3  class  3
3 c1 8706 . . 3  class  1
4 caddc 8708 . . 3  class  +
52, 3, 4co 5792 . 2  class  ( 3  +  1 )
61, 5wceq 1619 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  9787  4pos  9800  2p2e4  9809  3p1e4  9815  3p2e5  9822  4p4e8  9826  5p4e9  9829  6p4e10  9833  4nn  9846  3lt4  9856  halfpm6th  9903  7p4e11  10143  7p7e14  10146  8p4e12  10148  8p6e14  10150  9p4e13  10155  9p5e14  10156  4t4e16  10164  5t4e20  10166  6t4e24  10170  7t4e28  10175  8t4e32  10181  9t4e36  10188  ef4p  12355  ef01bndlem  12426  lt6abl  15143  iblitg  19085  sincosq4sgn  19831  ang180lem2  20070  binom4  20108  quart1lem  20113  log2cnv  20202  log2ub  20207  ppiublem2  20404  ppiub  20405  chtub  20413  bclbnd  20481  bposlem8  20492  lgsdir2lem3  20526  ipval2  21240  4bc2eq6  23470  bpoly3  24168  bpoly4  24169  fsumcube  24170  rmydioph  26474  rmxdioph  26476  expdiophlem2  26482  stoweidlem13  27097  stoweidlem34  27118
  Copyright terms: Public domain W3C validator