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

Definition df-4 8745
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 8737 . 2  class  4
2 c3 8736 . . 3  class  3
3 c1 7589 . . 3  class  1
4 caddc 7591 . . 3  class  +
52, 3, 4co 5742 . 2  class  ( 3  +  1 )
61, 5wceq 1316 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  8761  4pos  8781  2p2e4  8805  3p1e4  8813  3p2e5  8819  4p4e8  8823  5p4e9  8826  4nn  8841  3lt4  8850  halfpm6th  8898  6p4e10  9211  7p4e11  9215  7p7e14  9218  8p4e12  9221  8p6e14  9223  9p4e13  9228  9p5e14  9229  4t4e16  9238  5t4e20  9241  6t4e24  9245  7t4e28  9250  8t4e32  9256  9t4e36  9263  fzo0to42pr  9952  4bc2eq6  10475  ef4p  11314  ef01bndlem  11377  sincosq4sgn  12821
  Copyright terms: Public domain W3C validator