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

Definition df-4 10065
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 10056 . 2  class  4
2 c3 10055 . . 3  class  3
3 c1 8996 . . 3  class  1
4 caddc 8998 . . 3  class  +
52, 3, 4co 6084 . 2  class  ( 3  +  1 )
61, 5wceq 1653 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  10078  4pos  10091  2p2e4  10103  3p1e4  10109  3p2e5  10116  4p4e8  10120  5p4e9  10123  6p4e10  10127  4nn  10140  3lt4  10150  halfpm6th  10197  7p4e11  10439  7p7e14  10442  8p4e12  10444  8p6e14  10446  9p4e13  10451  9p5e14  10452  4t4e16  10460  5t4e20  10462  6t4e24  10466  7t4e28  10471  8t4e32  10477  9t4e36  10484  fzo0to42pr  11191  ef4p  12719  ef01bndlem  12790  lt6abl  15509  iblitg  19663  sincosq4sgn  20414  ang180lem2  20657  binom4  20695  quart1lem  20700  log2cnv  20789  log2ub  20794  ppiublem2  20992  ppiub  20993  chtub  21001  bclbnd  21069  bposlem8  21080  lgsdir2lem3  21114  usgraexvlem  21419  ipval2  22208  4bc2eq6  25209  bpoly3  26109  bpoly4  26110  fsumcube  26111  rmydioph  27099  rmxdioph  27101  expdiophlem2  27107  stoweidlem13  27752
  Copyright terms: Public domain W3C validator