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

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

Detailed syntax breakdown of Definition df-5
StepHypRef Expression
1 c5 8731 . 2 class 5
2 c4 8730 . . 3 class 4
3 c1 7585 . . 3 class 1
4 caddc 7587 . . 3 class +
52, 3, 4co 5740 . 2 class (4 + 1)
61, 5wceq 1314 1 wff 5 = (4 + 1)
Colors of variables: wff set class
This definition is referenced by:  5re  8756  5pos  8777  4p1e5  8807  3p2e5  8812  4p2e6  8814  5nn  8835  4lt5  8846  5p5e10  9203  6p5e11  9205  7p5e12  9209  8p5e13  9215  8p7e15  9217  9p5e14  9222  9p6e15  9223  5t5e25  9235  6t5e30  9239  7t5e35  9244  8t5e40  9250  9t5e45  9257  fldiv4p1lem1div2  10018  ef01bndlem  11362  ex-exp  12741  ex-fac  12742  ex-bc  12743
  Copyright terms: Public domain W3C validator