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

Definition df-5 10622
Description: Define the number 5. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-5

Detailed syntax breakdown of Definition df-5
StepHypRef Expression
1 c5 10613 . 2
2 c4 10612 . . 3
3 c1 9514 . . 3
4 caddc 9516 . . 3
52, 3, 4co 6296 . 2
61, 5wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  5re  10639  5pos  10658  4p1e5  10687  3p2e5  10693  4p2e6  10695  5p5e10  10701  5nn  10721  4lt5  10733  6p5e11  11054  7p5e12  11057  8p5e13  11062  8p7e15  11064  9p5e14  11069  9p6e15  11070  5t5e25  11080  6t5e30  11084  7t5e35  11089  8t5e40  11095  9t5e45  11102  ef01bndlem  13919  5prm  14594  lt6abl  16897  log2ublem3  23279  ppiublem2  23478  bclbnd  23555  bposlem6  23564  bposlem9  23567  lgsdir2lem3  23600  rmydioph  30956  expdiophlem2  30964  stoweidlem13  31795
  Copyright terms: Public domain W3C validator