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

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

Detailed syntax breakdown of Definition df-9
StepHypRef Expression
1 c9 11115 . 2 class 9
2 c8 11114 . . 3 class 8
3 c1 9975 . . 3 class 1
4 caddc 9977 . . 3 class +
52, 3, 4co 6690 . 2 class (8 + 1)
61, 5wceq 1523 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9re  11145  9pos  11160  9m1e8  11181  8p1e9  11196  5p4e9  11205  6p3e9  11208  7p2e9  11210  8p2e10OLD  11212  9nn  11230  8lt9  11260  8p2e10  11648  9p9e18  11665  9t9e81  11708  19prm  15872  139prm  15878  log2tlbnd  24717  bposlem8  25061  lgsdir2lem5  25099  2lgsoddprmlem3b  25181  2lgsoddprmlem3d  25183  rmydioph  37898  139prmALT  41836  9gbo  41987  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017
  Copyright terms: Public domain W3C validator