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 11080
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 11071 . 2 class 6
2 c5 11070 . . 3 class 5
3 c1 9934 . . 3 class 1
4 caddc 9936 . . 3 class +
52, 3, 4co 6647 . 2 class (5 + 1)
61, 5wceq 1482 1 wff 6 = (5 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  6re  11098  6pos  11116  6m1e5  11137  5p1e6  11152  3p3e6  11158  4p2e6  11159  5p2e7  11162  6nn  11186  5lt6  11201  6p6e12  11599  7p6e13  11605  8p6e14  11613  8p8e16  11615  9p6e15  11621  9p7e16  11622  6t6e36  11643  6t6e36OLD  11644  7t6e42  11649  8t6e48  11656  8t6e48OLD  11657  9t6e54  11664  lt6abl  18290  ppiublem1  24921  ppiublem2  24922  ppiub  24923  bposlem8  25010  lgsdir2lem3  25046  2lgsoddprmlem3d  25132  rmydioph  37407  expdiophlem2  37415  stgoldbwt  41435  sbgoldbm  41443
  Copyright terms: Public domain W3C validator