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 11043
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 11034 . 2 class 6
2 c5 11033 . . 3 class 5
3 c1 9897 . . 3 class 1
4 caddc 9899 . . 3 class +
52, 3, 4co 6615 . 2 class (5 + 1)
61, 5wceq 1480 1 wff 6 = (5 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  6re  11061  6pos  11079  6m1e5  11100  5p1e6  11115  3p3e6  11121  4p2e6  11122  5p2e7  11125  6nn  11149  5lt6  11164  6p6e12  11562  7p6e13  11568  8p6e14  11576  8p8e16  11578  9p6e15  11584  9p7e16  11585  6t6e36  11606  6t6e36OLD  11607  7t6e42  11612  8t6e48  11619  8t6e48OLD  11620  9t6e54  11627  lt6abl  18236  ppiublem1  24861  ppiublem2  24862  ppiub  24863  bposlem8  24950  lgsdir2lem3  24986  2lgsoddprmlem3d  25072  rmydioph  37100  expdiophlem2  37108  stgoldbwt  40989
  Copyright terms: Public domain W3C validator