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

Definition df-4 10060
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 10051 . 2  class  4
2 c3 10050 . . 3  class  3
3 c1 8991 . . 3  class  1
4 caddc 8993 . . 3  class  +
52, 3, 4co 6081 . 2  class  ( 3  +  1 )
61, 5wceq 1652 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  10073  4pos  10086  2p2e4  10098  3p1e4  10104  3p2e5  10111  4p4e8  10115  5p4e9  10118  6p4e10  10122  4nn  10135  3lt4  10145  halfpm6th  10192  7p4e11  10434  7p7e14  10437  8p4e12  10439  8p6e14  10441  9p4e13  10446  9p5e14  10447  4t4e16  10455  5t4e20  10457  6t4e24  10461  7t4e28  10466  8t4e32  10472  9t4e36  10479  fzo0to42pr  11186  ef4p  12714  ef01bndlem  12785  lt6abl  15504  iblitg  19660  sincosq4sgn  20409  ang180lem2  20652  binom4  20690  quart1lem  20695  log2cnv  20784  log2ub  20789  ppiublem2  20987  ppiub  20988  chtub  20996  bclbnd  21064  bposlem8  21075  lgsdir2lem3  21109  usgraexvlem  21414  ipval2  22203  4bc2eq6  25204  bpoly3  26104  bpoly4  26105  fsumcube  26106  rmydioph  27085  rmxdioph  27087  expdiophlem2  27093  stoweidlem13  27738
  Copyright terms: Public domain W3C validator