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

Definition df-5 8484
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 8476 . 2 class 5
2 c4 8475 . . 3 class 4
3 c1 7351 . . 3 class 1
4 caddc 7353 . . 3 class +
52, 3, 4co 5652 . 2 class (4 + 1)
61, 5wceq 1289 1 wff 5 = (4 + 1)
Colors of variables: wff set class
This definition is referenced by:  5re  8501  5pos  8522  4p1e5  8552  3p2e5  8557  4p2e6  8559  5nn  8580  4lt5  8591  5p5e10  8947  6p5e11  8949  7p5e12  8953  8p5e13  8959  8p7e15  8961  9p5e14  8966  9p6e15  8967  5t5e25  8979  6t5e30  8983  7t5e35  8988  8t5e40  8994  9t5e45  9001  fldiv4p1lem1div2  9712  ef01bndlem  11047  ex-exp  11654  ex-fac  11655  ex-bc  11656
  Copyright terms: Public domain W3C validator