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

Definition df-4 10052
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 10043 . 2  class  4
2 c3 10042 . . 3  class  3
3 c1 8983 . . 3  class  1
4 caddc 8985 . . 3  class  +
52, 3, 4co 6073 . 2  class  ( 3  +  1 )
61, 5wceq 1652 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  10065  4pos  10078  2p2e4  10090  3p1e4  10096  3p2e5  10103  4p4e8  10107  5p4e9  10110  6p4e10  10114  4nn  10127  3lt4  10137  halfpm6th  10184  7p4e11  10426  7p7e14  10429  8p4e12  10431  8p6e14  10433  9p4e13  10438  9p5e14  10439  4t4e16  10447  5t4e20  10449  6t4e24  10453  7t4e28  10458  8t4e32  10464  9t4e36  10471  fzo0to42pr  11178  ef4p  12706  ef01bndlem  12777  lt6abl  15496  iblitg  19652  sincosq4sgn  20401  ang180lem2  20644  binom4  20682  quart1lem  20687  log2cnv  20776  log2ub  20781  ppiublem2  20979  ppiub  20980  chtub  20988  bclbnd  21056  bposlem8  21067  lgsdir2lem3  21101  usgraexvlem  21406  ipval2  22195  4bc2eq6  25196  bpoly3  26096  bpoly4  26097  fsumcube  26098  rmydioph  27076  rmxdioph  27078  expdiophlem2  27084  stoweidlem13  27729
  Copyright terms: Public domain W3C validator