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

Definition df-4 8804
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 8796 . 2  class  4
2 c3 8795 . . 3  class  3
3 c1 7644 . . 3  class  1
4 caddc 7646 . . 3  class  +
52, 3, 4co 5781 . 2  class  ( 3  +  1 )
61, 5wceq 1332 1  wff  4  =  ( 3  +  1 )
Colors of variables: wff set class
This definition is referenced by:  4re  8820  4pos  8840  4m1e3  8864  2p2e4  8870  3p1e4  8878  3p2e5  8884  4p4e8  8888  5p4e9  8891  4nn  8906  3lt4  8915  halfpm6th  8963  6p4e10  9276  7p4e11  9280  7p7e14  9283  8p4e12  9286  8p6e14  9288  9p4e13  9293  9p5e14  9294  4t4e16  9303  5t4e20  9306  6t4e24  9310  7t4e28  9315  8t4e32  9321  9t4e36  9328  fzo0to42pr  10027  4bc2eq6  10551  ef4p  11435  ef01bndlem  11497  sincosq4sgn  12956
  Copyright terms: Public domain W3C validator