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 10841
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 10832 . 2 class 5
2 c4 10831 . . 3 class 4
3 c1 9696 . . 3 class 1
4 caddc 9698 . . 3 class +
52, 3, 4co 6431 . 2 class (4 + 1)
61, 5wceq 1474 1 wff 5 = (4 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  5re  10858  5pos  10877  5m1e4  10898  4p1e5  10913  3p2e5  10919  4p2e6  10921  5p5e10OLD  10927  5nn  10947  4lt5  10959  5p5e10  11340  6p5e11  11344  6p5e11OLD  11345  7p5e12  11351  8p5e13  11359  8p7e15  11361  9p5e14  11367  9p6e15  11368  5t5e25  11383  5t5e25OLD  11384  6t5e30  11388  6t5e30OLD  11389  7t5e35  11395  8t5e40  11401  8t5e40OLD  11402  9t5e45  11410  fldiv4p1lem1div2  12370  ef01bndlem  14626  prm23lt5  15245  5prm  15541  lt6abl  18030  log2ublem3  24366  ppiublem2  24621  bclbnd  24698  bposlem6  24707  bposlem9  24710  lgsdir2lem3  24745  2lgslem3c  24816  2lgsoddprmlem3c  24830  ex-exp  26441  ex-fac  26442  ex-bc  26443  rmydioph  36493  expdiophlem2  36501  stoweidlem13  38813  fmtno5  39919  fmtnofac1  39932  31prm  39962  5odd  40069
  Copyright terms: Public domain W3C validator