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

Definition df-4 7735
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 7726 . 2 class 4
2 c3 7725 . . 3 class 3
3 c1 6692 . . 3 class 1
4 caddc 6694 . . 3 class +
52, 3, 4co 5455 . 2 class (3 + 1)
61, 5wceq 1242 1 wff 4 = (3 + 1)
Colors of variables: wff set class
This definition is referenced by:  4re  7752  4pos  7772  2p2e4  7795  3p1e4  7803  3p2e5  7810  4p4e8  7814  5p4e9  7817  6p4e10  7821  4nn  7837  3lt4  7847  halfpm6th  7902  7p4e11  8175  7p7e14  8178  8p4e12  8180  8p6e14  8182  9p4e13  8187  9p5e14  8188  4t4e16  8196  5t4e20  8198  6t4e24  8202  7t4e28  8207  8t4e32  8213  9t4e36  8220  fzo0to42pr  8826
  Copyright terms: Public domain W3C validator