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

Definition df-4 8639
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 8631 . 2  class  4
2 c3 8630 . . 3  class  3
3 c1 7501 . . 3  class  1
4 caddc 7503 . . 3  class  +
52, 3, 4co 5706 . 2  class  ( 3  +  1 )
61, 5wceq 1299 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  8655  4pos  8675  2p2e4  8699  3p1e4  8707  3p2e5  8713  4p4e8  8717  5p4e9  8720  4nn  8735  3lt4  8744  halfpm6th  8792  6p4e10  9105  7p4e11  9109  7p7e14  9112  8p4e12  9115  8p6e14  9117  9p4e13  9122  9p5e14  9123  4t4e16  9132  5t4e20  9135  6t4e24  9139  7t4e28  9144  8t4e32  9150  9t4e36  9157  fzo0to42pr  9838  4bc2eq6  10361  ef4p  11198  ef01bndlem  11261
  Copyright terms: Public domain W3C validator