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

Definition df-5 10468
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 10459 . 2
2 c4 10458 . . 3
3 c1 9368 . . 3
4 caddc 9370 . . 3
52, 3, 4co 6174 . 2
61, 5wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  5re  10485  5pos  10504  4p1e5  10533  3p2e5  10539  4p2e6  10541  5p5e10  10547  5nn  10567  4lt5  10579  6p5e11  10890  7p5e12  10893  8p5e13  10898  8p7e15  10900  9p5e14  10905  9p6e15  10906  5t5e25  10916  6t5e30  10920  7t5e35  10925  8t5e40  10931  9t5e45  10938  ef01bndlem  13554  5prm  14222  lt6abl  16459  log2ublem3  22443  ppiublem2  22642  bclbnd  22719  bposlem6  22728  bposlem9  22731  lgsdir2lem3  22764  rmydioph  29485  expdiophlem2  29493  stoweidlem13  29930
  Copyright terms: Public domain W3C validator