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 12336
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 12328 . 2 class 9
2 c8 12327 . . 3 class 8
3 c1 11156 . . 3 class 1
4 caddc 11158 . . 3 class +
52, 3, 4co 7431 . 2 class (8 + 1)
61, 5wceq 1540 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9nn  12364  9re  12365  9cn  12366  9pos  12379  9m1e8  12400  8p1e9  12416  5p4e9  12424  6p3e9  12426  7p2e9  12427  8lt9  12465  8p2e10  12813  9p9e18  12827  9t9e81  12862  19prm  17155  139prm  17161  bposlem8  27335  lgsdir2lem5  27373  2lgsoddprmlem3d  27457  aks4d1p1  42077  rmydioph  43026  139prmALT  47583  9gbo  47761  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791
  Copyright terms: Public domain W3C validator