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

Definition df-4 8969
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 8961 . 2 class 4
2 c3 8960 . . 3 class 3
3 c1 7803 . . 3 class 1
4 caddc 7805 . . 3 class +
52, 3, 4co 5869 . 2 class (3 + 1)
61, 5wceq 1353 1 wff 4 = (3 + 1)
Colors of variables: wff set class
This definition is referenced by:  4re  8985  4pos  9005  4m1e3  9029  2p2e4  9035  3p1e4  9043  3p2e5  9049  4p4e8  9053  5p4e9  9056  4nn  9071  3lt4  9080  halfpm6th  9128  6p4e10  9444  7p4e11  9448  7p7e14  9451  8p4e12  9454  8p6e14  9456  9p4e13  9461  9p5e14  9462  4t4e16  9471  5t4e20  9474  6t4e24  9478  7t4e28  9483  8t4e32  9489  9t4e36  9496  fz0to4untppr  10110  fzo0to42pr  10206  4bc2eq6  10738  ef4p  11686  ef01bndlem  11748  sincosq4sgn  13917  binom4  14064  lgsdir2lem3  14098
  Copyright terms: Public domain W3C validator