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 10926
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 10917 . 2 class 6
2 c5 10916 . . 3 class 5
3 c1 9789 . . 3 class 1
4 caddc 9791 . . 3 class +
52, 3, 4co 6523 . 2 class (5 + 1)
61, 5wceq 1474 1 wff 6 = (5 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  6re  10944  6pos  10962  6m1e5  10983  5p1e6  10998  3p3e6  11004  4p2e6  11005  5p2e7  11008  6nn  11032  5lt6  11047  6p6e12  11430  7p6e13  11436  8p6e14  11444  8p8e16  11446  9p6e15  11452  9p7e16  11453  6t6e36  11474  6t6e36OLD  11475  7t6e42  11480  8t6e48  11487  8t6e48OLD  11488  9t6e54  11495  lt6abl  18061  ppiublem1  24640  ppiublem2  24641  ppiub  24642  bposlem8  24729  lgsdir2lem3  24765  2lgsoddprmlem3d  24851  rmydioph  36398  expdiophlem2  36406  stgoldbwt  39999
  Copyright terms: Public domain W3C validator