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

Definition df-4 9010
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 9002 . 2  class  4
2 c3 9001 . . 3  class  3
3 c1 7842 . . 3  class  1
4 caddc 7844 . . 3  class  +
52, 3, 4co 5896 . 2  class  ( 3  +  1 )
61, 5wceq 1364 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  9026  4pos  9046  4m1e3  9070  2p2e4  9076  3p1e4  9084  3p2e5  9090  4p4e8  9094  5p4e9  9097  4nn  9112  3lt4  9121  halfpm6th  9169  6p4e10  9485  7p4e11  9489  7p7e14  9492  8p4e12  9495  8p6e14  9497  9p4e13  9502  9p5e14  9503  4t4e16  9512  5t4e20  9515  6t4e24  9519  7t4e28  9524  8t4e32  9530  9t4e36  9537  fz0to4untppr  10154  fzo0to42pr  10250  4bc2eq6  10786  ef4p  11734  ef01bndlem  11796  sincosq4sgn  14710  binom4  14857  lgsdir2lem3  14892
  Copyright terms: Public domain W3C validator