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

Definition df-5 8750
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 8742 . 2 class 5
2 c4 8741 . . 3 class 4
3 c1 7589 . . 3 class 1
4 caddc 7591 . . 3 class +
52, 3, 4co 5742 . 2 class (4 + 1)
61, 5wceq 1316 1 wff 5 = (4 + 1)
Colors of variables: wff set class
This definition is referenced by:  5re  8767  5pos  8788  5m1e4  8810  4p1e5  8824  3p2e5  8829  4p2e6  8831  5nn  8852  4lt5  8863  5p5e10  9220  6p5e11  9222  7p5e12  9226  8p5e13  9232  8p7e15  9234  9p5e14  9239  9p6e15  9240  5t5e25  9252  6t5e30  9256  7t5e35  9261  8t5e40  9267  9t5e45  9274  fldiv4p1lem1div2  10046  ef01bndlem  11390  ex-exp  12866  ex-fac  12867  ex-bc  12868
  Copyright terms: Public domain W3C validator