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 10933
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 10924 . 2 class 9
2 c8 10923 . . 3 class 8
3 c1 9793 . . 3 class 1
4 caddc 9795 . . 3 class +
52, 3, 4co 6527 . 2 class (8 + 1)
61, 5wceq 1474 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9re  10954  9pos  10969  9m1e8  10990  8p1e9  11005  5p4e9  11014  6p3e9  11017  7p2e9  11019  8p2e10OLD  11021  9nn  11039  8lt9  11069  8p2e10  11442  9p9e18  11459  9t9e81  11502  19prm  15609  139prm  15615  log2tlbnd  24389  bposlem8  24733  lgsdir2lem5  24771  2lgsoddprmlem3b  24853  2lgsoddprmlem3d  24855  rmydioph  36395  139prmALT  39847  9gboa  39994  wtgoldbnnsum4prm  40016  bgoldbnnsum3prm  40018
  Copyright terms: Public domain W3C validator