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 10963
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 10954 . 2 class 9
2 c8 10953 . . 3 class 8
3 c1 9816 . . 3 class 1
4 caddc 9818 . . 3 class +
52, 3, 4co 6549 . 2 class (8 + 1)
61, 5wceq 1475 1 wff 9 = (8 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  9re  10984  9pos  10999  9m1e8  11020  8p1e9  11035  5p4e9  11044  6p3e9  11047  7p2e9  11049  8p2e10OLD  11051  9nn  11069  8lt9  11099  8p2e10  11486  9p9e18  11503  9t9e81  11546  19prm  15663  139prm  15669  log2tlbnd  24472  bposlem8  24816  lgsdir2lem5  24854  2lgsoddprmlem3b  24936  2lgsoddprmlem3d  24938  rmydioph  36599  139prmALT  40049  9gboa  40196  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220
  Copyright terms: Public domain W3C validator