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 12315
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 12307 . 2 class 9
2 c8 12306 . . 3 class 8
3 c1 11141 . . 3 class 1
4 caddc 11143 . . 3 class +
52, 3, 4co 7419 . 2 class (8 + 1)
61, 5wceq 1533 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9nn  12343  9re  12344  9cn  12345  9pos  12358  9m1e8  12379  8p1e9  12395  5p4e9  12403  6p3e9  12405  7p2e9  12406  8lt9  12444  8p2e10  12790  9p9e18  12804  9t9e81  12839  19prm  17090  139prm  17096  bposlem8  27269  lgsdir2lem5  27307  2lgsoddprmlem3d  27391  aks4d1p1  41679  rmydioph  42577  139prmALT  47073  9gbo  47251  wtgoldbnnsum4prm  47279  bgoldbnnsum3prm  47281
  Copyright terms: Public domain W3C validator