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

Definition df-5 11026
Description: Define the number 5. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-5 5 = (4 + 1)

Detailed syntax breakdown of Definition df-5
StepHypRef Expression
1 c5 11017 . 2 class 5
2 c4 11016 . . 3 class 4
3 c1 9881 . . 3 class 1
4 caddc 9883 . . 3 class +
52, 3, 4co 6604 . 2 class (4 + 1)
61, 5wceq 1480 1 wff 5 = (4 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  5re  11043  5pos  11062  5m1e4  11083  4p1e5  11098  3p2e5  11104  4p2e6  11106  5p5e10OLD  11112  5nn  11132  4lt5  11144  5p5e10  11540  6p5e11  11544  6p5e11OLD  11545  7p5e12  11551  8p5e13  11559  8p7e15  11561  9p5e14  11567  9p6e15  11568  5t5e25  11583  5t5e25OLD  11584  6t5e30  11588  6t5e30OLD  11589  7t5e35  11595  8t5e40  11601  8t5e40OLD  11602  9t5e45  11610  fldiv4p1lem1div2  12576  ef01bndlem  14839  prm23lt5  15443  5prm  15739  lt6abl  18217  log2ublem3  24575  ppiublem2  24828  bclbnd  24905  bposlem6  24914  bposlem9  24917  lgsdir2lem3  24952  2lgslem3c  25023  2lgsoddprmlem3c  25037  ex-exp  27161  ex-fac  27162  ex-bc  27163  rmydioph  37058  expdiophlem2  37066  stoweidlem13  39534  fmtno5  40765  fmtnofac1  40778  31prm  40808  5odd  40915
  Copyright terms: Public domain W3C validator