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

Definition df-4 10016
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 10007 . 2  class  4
2 c3 10006 . . 3  class  3
3 c1 8947 . . 3  class  1
4 caddc 8949 . . 3  class  +
52, 3, 4co 6040 . 2  class  ( 3  +  1 )
61, 5wceq 1649 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  10029  4pos  10042  2p2e4  10054  3p1e4  10060  3p2e5  10067  4p4e8  10071  5p4e9  10074  6p4e10  10078  4nn  10091  3lt4  10101  halfpm6th  10148  7p4e11  10390  7p7e14  10393  8p4e12  10395  8p6e14  10397  9p4e13  10402  9p5e14  10403  4t4e16  10411  5t4e20  10413  6t4e24  10417  7t4e28  10422  8t4e32  10428  9t4e36  10435  fzo0to42pr  11141  ef4p  12669  ef01bndlem  12740  lt6abl  15459  iblitg  19613  sincosq4sgn  20362  ang180lem2  20605  binom4  20643  quart1lem  20648  log2cnv  20737  log2ub  20742  ppiublem2  20940  ppiub  20941  chtub  20949  bclbnd  21017  bposlem8  21028  lgsdir2lem3  21062  usgraexvlem  21367  ipval2  22156  4bc2eq6  25157  bpoly3  26008  bpoly4  26009  fsumcube  26010  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  stoweidlem13  27629
  Copyright terms: Public domain W3C validator