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

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

Detailed syntax breakdown of Definition df-4
StepHypRef Expression
1 c4 8158 . 2 class 4
2 c3 8157 . . 3 class 3
3 c1 7044 . . 3 class 1
4 caddc 7046 . . 3 class +
52, 3, 4co 5543 . 2 class (3 + 1)
61, 5wceq 1285 1 wff 4 = (3 + 1)
Colors of variables: wff set class
This definition is referenced by:  4re  8183  4pos  8203  2p2e4  8226  3p1e4  8234  3p2e5  8240  4p4e8  8244  5p4e9  8247  4nn  8262  3lt4  8271  halfpm6th  8318  6p4e10  8629  7p4e11  8633  7p7e14  8636  8p4e12  8639  8p6e14  8641  9p4e13  8646  9p5e14  8647  4t4e16  8656  5t4e20  8659  6t4e24  8663  7t4e28  8668  8t4e32  8674  9t4e36  8681  fzo0to42pr  9306  4bc2eq6  9798
  Copyright terms: Public domain W3C validator