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 11504
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 11496 . 2 class 9
2 c8 11495 . . 3 class 8
3 c1 10330 . . 3 class 1
4 caddc 10332 . . 3 class +
52, 3, 4co 6970 . 2 class (8 + 1)
61, 5wceq 1507 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9nn  11538  9re  11539  9cn  11540  9pos  11554  9m1e8  11575  8p1e9  11591  5p4e9  11599  6p3e9  11601  7p2e9  11602  8lt9  11640  8p2e10  11987  9p9e18  12001  9t9e81  12036  19prm  16301  139prm  16307  bposlem8  25563  lgsdir2lem5  25601  2lgsoddprmlem3d  25685  rmydioph  39007  139prmALT  43127  9gbo  43307  wtgoldbnnsum4prm  43335  bgoldbnnsum3prm  43337
  Copyright terms: Public domain W3C validator