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

Definition df-5 8412
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 8403 . 2  class  5
2 c4 8402 . . 3  class  4
3 c1 7288 . . 3  class  1
4 caddc 7290 . . 3  class  +
52, 3, 4co 5607 . 2  class  ( 4  +  1 )
61, 5wceq 1287 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  8429  5pos  8450  4p1e5  8479  3p2e5  8484  4p2e6  8486  5nn  8507  4lt5  8518  5p5e10  8872  6p5e11  8874  7p5e12  8878  8p5e13  8884  8p7e15  8886  9p5e14  8891  9p6e15  8892  5t5e25  8904  6t5e30  8908  7t5e35  8913  8t5e40  8919  9t5e45  8926  fldiv4p1lem1div2  9633  ex-fac  11085  ex-bc  11086
  Copyright terms: Public domain W3C validator