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

Definition df-4 9204
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 9196 . 2  class  4
2 c3 9195 . . 3  class  3
3 c1 8033 . . 3  class  1
4 caddc 8035 . . 3  class  +
52, 3, 4co 6018 . 2  class  ( 3  +  1 )
61, 5wceq 1397 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  9220  4pos  9240  4m1e3  9264  2p2e4  9270  3p1e4  9279  3p2e5  9285  4p4e8  9289  5p4e9  9292  4nn  9307  3lt4  9316  halfpm6th  9364  6p4e10  9682  7p4e11  9686  7p7e14  9689  8p4e12  9692  8p6e14  9694  9p4e13  9699  9p5e14  9700  4t4e16  9709  5t4e20  9712  6t4e24  9716  7t4e28  9721  8t4e32  9727  9t4e36  9734  fz0to4untppr  10359  fzo0to42pr  10465  4bc2eq6  11036  ef4p  12256  ef01bndlem  12318  sincosq4sgn  15555  binom4  15705  lgsdir2lem3  15761
  Copyright terms: Public domain W3C validator