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

Definition df-5 10329
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 10320 . 2
2 c4 10319 . . 3
3 c1 9229 . . 3
4 caddc 9231 . . 3
52, 3, 4co 6061 . 2
61, 5wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  5re  10346  5pos  10365  4p1e5  10394  3p2e5  10400  4p2e6  10402  5p5e10  10408  5nn  10428  4lt5  10440  6p5e11  10750  7p5e12  10753  8p5e13  10758  8p7e15  10760  9p5e14  10765  9p6e15  10766  5t5e25  10776  6t5e30  10780  7t5e35  10785  8t5e40  10791  9t5e45  10798  ef01bndlem  13408  5prm  14076  lt6abl  16307  log2ublem3  22084  ppiublem2  22283  bclbnd  22360  bposlem6  22369  bposlem9  22372  lgsdir2lem3  22405  rmydioph  29036  expdiophlem2  29044  stoweidlem13  29482
  Copyright terms: Public domain W3C validator