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 11696
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 11688 . 2 class 9
2 c8 11687 . . 3 class 8
3 c1 10527 . . 3 class 1
4 caddc 10529 . . 3 class +
52, 3, 4co 7145 . 2 class (8 + 1)
61, 5wceq 1528 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9nn  11724  9re  11725  9cn  11726  9pos  11739  9m1e8  11760  8p1e9  11776  5p4e9  11784  6p3e9  11786  7p2e9  11787  8lt9  11825  8p2e10  12167  9p9e18  12181  9t9e81  12216  19prm  16441  139prm  16447  bposlem8  25795  lgsdir2lem5  25833  2lgsoddprmlem3d  25917  rmydioph  39491  139prmALT  43606  9gbo  43786  wtgoldbnnsum4prm  43814  bgoldbnnsum3prm  43816
  Copyright terms: Public domain W3C validator