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

Definition df-8 8797
Description: Define the number 8. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-8 8 = (7 + 1)

Detailed syntax breakdown of Definition df-8
StepHypRef Expression
1 c8 8789 . 2 class 8
2 c7 8788 . . 3 class 7
3 c1 7633 . . 3 class 1
4 caddc 7635 . . 3 class +
52, 3, 4co 5774 . 2 class (7 + 1)
61, 5wceq 1331 1 wff 8 = (7 + 1)
Colors of variables: wff set class
This definition is referenced by:  8re  8817  8pos  8835  8m1e7  8857  7p1e8  8871  4p4e8  8877  5p3e8  8879  6p2e8  8881  7p2e9  8883  8nn  8899  7lt8  8922  8p8e16  9279  9p8e17  9286  9p9e18  9287  8t8e64  9314  9t8e72  9321
  Copyright terms: Public domain W3C validator