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 10960
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 10951 . 2 class 6
2 c5 10950 . . 3 class 5
3 c1 9816 . . 3 class 1
4 caddc 9818 . . 3 class +
52, 3, 4co 6549 . 2 class (5 + 1)
61, 5wceq 1475 1 wff 6 = (5 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  6re  10978  6pos  10996  6m1e5  11017  5p1e6  11032  3p3e6  11038  4p2e6  11039  5p2e7  11042  6nn  11066  5lt6  11081  6p6e12  11478  7p6e13  11484  8p6e14  11492  8p8e16  11494  9p6e15  11500  9p7e16  11501  6t6e36  11522  6t6e36OLD  11523  7t6e42  11528  8t6e48  11535  8t6e48OLD  11536  9t6e54  11543  lt6abl  18119  ppiublem1  24727  ppiublem2  24728  ppiub  24729  bposlem8  24816  lgsdir2lem3  24852  2lgsoddprmlem3d  24938  rmydioph  36599  expdiophlem2  36607  stgoldbwt  40198
  Copyright terms: Public domain W3C validator