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

Definition df-8 8983
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 8975 . 2 class 8
2 c7 8974 . . 3 class 7
3 c1 7811 . . 3 class 1
4 caddc 7813 . . 3 class +
52, 3, 4co 5874 . 2 class (7 + 1)
61, 5wceq 1353 1 wff 8 = (7 + 1)
Colors of variables: wff set class
This definition is referenced by:  8re  9003  8pos  9021  8m1e7  9043  7p1e8  9057  4p4e8  9063  5p3e8  9065  6p2e8  9067  7p2e9  9069  8nn  9085  7lt8  9108  8p8e16  9468  9p8e17  9475  9p9e18  9476  8t8e64  9503  9t8e72  9510
  Copyright terms: Public domain W3C validator