ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-6 Unicode version

Definition df-6 8985
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 8977 . 2  class  6
2 c5 8976 . . 3  class  5
3 c1 7815 . . 3  class  1
4 caddc 7817 . . 3  class  +
52, 3, 4co 5878 . 2  class  ( 5  +  1 )
61, 5wceq 1353 1  wff  6  =  ( 5  +  1 )
Colors of variables: wff set class
This definition is referenced by:  6re  9003  6pos  9023  6m1e5  9045  5p1e6  9059  3p3e6  9064  4p2e6  9065  5p2e7  9068  6nn  9087  5lt6  9101  6p6e12  9460  7p6e13  9464  8p6e14  9470  8p8e16  9472  9p6e15  9477  9p7e16  9478  6t6e36  9494  7t6e42  9499  8t6e48  9505  9t6e54  9512  lgsdir2lem3  14619  2lgsoddprmlem3d  14646
  Copyright terms: Public domain W3C validator