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 11367
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 11359 . 2 class 9
2 c8 11358 . . 3 class 8
3 c1 10218 . . 3 class 1
4 caddc 10220 . . 3 class +
52, 3, 4co 6870 . 2 class (8 + 1)
61, 5wceq 1637 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9re  11387  9pos  11401  9m1e8  11422  8p1e9  11437  5p4e9  11445  6p3e9  11447  7p2e9  11448  9nn  11465  8lt9  11494  8p2e10  11835  9p9e18  11849  9t9e81  11884  19prm  16032  139prm  16038  log2tlbnd  24882  bposlem8  25226  lgsdir2lem5  25264  2lgsoddprmlem3b  25346  2lgsoddprmlem3d  25348  rmydioph  38076  139prmALT  42080  9gbo  42231  wtgoldbnnsum4prm  42259  bgoldbnnsum3prm  42261
  Copyright terms: Public domain W3C validator