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

Definition df-4 11691
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 11683 . 2 class 4
2 c3 11682 . . 3 class 3
3 c1 10527 . . 3 class 1
4 caddc 10529 . . 3 class +
52, 3, 4co 7145 . 2 class (3 + 1)
61, 5wceq 1528 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4nn  11709  4re  11710  4cn  11711  4pos  11733  4m1e3  11755  2p2e4  11761  3p1e4  11771  3p2e5  11777  4p4e8  11781  5p4e9  11784  3lt4  11800  halfpm6th  11847  6p4e10  12159  7p4e11  12163  7p7e14  12166  8p4e12  12169  8p6e14  12171  9p4e13  12176  9p5e14  12177  4t4e16  12186  5t4e20  12189  6t4e24  12193  7t4e28  12198  8t4e32  12204  9t4e36  12211  fz0to4untppr  13000  4bc2eq6  13679  bpoly3  15402  bpoly4  15403  fsumcube  15404  ef4p  15456  ef01bndlem  15527  ge2nprmge4  16035  lt6abl  18946  cphipval  23775  sincosq4sgn  25016  binom4  25355  quart1lem  25360  log2cnv  25450  ppiublem2  25707  ppiub  25708  chtub  25716  bclbnd  25784  bposlem8  25795  lgsdir2lem3  25831  3wlkdlem1  27866  ipval2  28412  problem3  32808  rmydioph  39491  rmxdioph  39493  expdiophlem2  39499  lt4addmuld  41453  stoweidlem13  42179  4even  43721  sbgoldbo  43799
  Copyright terms: Public domain W3C validator