MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-6 Structured version   Visualization version   GIF version

Definition df-6 11375
Description: Define the number 6. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-6 6 = (5 + 1)

Detailed syntax breakdown of Definition df-6
StepHypRef Expression
1 c6 11367 . 2 class 6
2 c5 11366 . . 3 class 5
3 c1 10229 . . 3 class 1
4 caddc 10231 . . 3 class +
52, 3, 4co 6881 . 2 class (5 + 1)
61, 5wceq 1637 1 wff 6 = (5 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  6re  11392  6pos  11409  6m1e5  11430  5p1e6  11445  3p3e6  11450  4p2e6  11451  5p2e7  11454  6nn  11473  5lt6  11487  6p6e12  11840  7p6e13  11844  8p6e14  11850  8p8e16  11852  9p6e15  11857  9p7e16  11858  6t6e36  11874  7t6e42  11879  8t6e48  11885  9t6e54  11892  lt6abl  18504  ppiublem1  25151  ppiublem2  25152  ppiub  25153  bposlem8  25240  lgsdir2lem3  25276  2lgsoddprmlem3d  25362  rmydioph  38087  expdiophlem2  38095  stgoldbwt  42244  sbgoldbm  42252
  Copyright terms: Public domain W3C validator