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 11066
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 11057 . 2 class 4
2 c3 11056 . . 3 class 3
3 c1 9922 . . 3 class 1
4 caddc 9924 . . 3 class +
52, 3, 4co 6635 . 2 class (3 + 1)
61, 5wceq 1481 1 wff 4 = (3 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  4re  11082  4pos  11101  4m1e3  11123  2p2e4  11129  3p1e4  11138  3p2e5  11145  4p4e8  11149  5p4e9  11152  6p4e10OLD  11156  4nn  11172  3lt4  11182  halfpm6th  11238  6p4e10  11583  7p4e11  11590  7p4e11OLD  11591  7p7e14  11594  8p4e12  11599  8p6e14  11601  9p4e13  11607  9p5e14  11608  4t4e16  11618  5t4e20  11622  5t4e20OLD  11623  6t4e24  11628  7t4e28  11635  8t4e32  11641  9t4e36  11650  fz0to4untppr  12426  fzo0to42pr  12539  4bc2eq6  13099  bpoly3  14770  bpoly4  14771  fsumcube  14772  ef4p  14824  ef01bndlem  14895  lt6abl  18277  cphipval  23023  iblitg  23516  sincosq4sgn  24234  ang180lem2  24521  binom4  24558  quart1lem  24563  log2cnv  24652  ppiublem2  24909  ppiub  24910  chtub  24918  bclbnd  24986  bposlem8  24997  lgsdir2lem3  25033  3wlkdlem1  26999  ipval2  27532  problem3  31535  rmydioph  37400  rmxdioph  37402  expdiophlem2  37408  lt4addmuld  39333  stoweidlem13  39993  4even  41383  sbgoldbo  41440
  Copyright terms: Public domain W3C validator