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 11695
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 11687 . 2 class 9
2 c8 11686 . . 3 class 8
3 c1 10527 . . 3 class 1
4 caddc 10529 . . 3 class +
52, 3, 4co 7135 . 2 class (8 + 1)
61, 5wceq 1538 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9nn  11723  9re  11724  9cn  11725  9pos  11738  9m1e8  11759  8p1e9  11775  5p4e9  11783  6p3e9  11785  7p2e9  11786  8lt9  11824  8p2e10  12166  9p9e18  12180  9t9e81  12215  19prm  16443  139prm  16449  bposlem8  25875  lgsdir2lem5  25913  2lgsoddprmlem3d  25997  rmydioph  39953  139prmALT  44111  9gbo  44290  wtgoldbnnsum4prm  44318  bgoldbnnsum3prm  44320
  Copyright terms: Public domain W3C validator