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

Definition df-5 7974
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 7965 . 2 class 5
2 c4 7964 . . 3 class 4
3 c1 6888 . . 3 class 1
4 caddc 6890 . . 3 class +
52, 3, 4co 5512 . 2 class (4 + 1)
61, 5wceq 1243 1 wff 5 = (4 + 1)
Colors of variables: wff set class
This definition is referenced by:  5re  7992  5pos  8014  4p1e5  8044  3p2e5  8050  4p2e6  8052  5p5e10  8058  5nn  8078  4lt5  8090  6p5e11  8415  7p5e12  8418  8p5e13  8423  8p7e15  8425  9p5e14  8430  9p6e15  8431  5t5e25  8441  6t5e30  8445  7t5e35  8450  8t5e40  8456  9t5e45  8463  fldiv4p1lem1div2  9145
  Copyright terms: Public domain W3C validator