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

Definition df-4 8800
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 8792 . 2 class 4
2 c3 8791 . . 3 class 3
3 c1 7640 . . 3 class 1
4 caddc 7642 . . 3 class +
52, 3, 4co 5777 . 2 class (3 + 1)
61, 5wceq 1331 1 wff 4 = (3 + 1)
Colors of variables: wff set class
This definition is referenced by:  4re  8816  4pos  8836  4m1e3  8860  2p2e4  8866  3p1e4  8874  3p2e5  8880  4p4e8  8884  5p4e9  8887  4nn  8902  3lt4  8911  halfpm6th  8959  6p4e10  9272  7p4e11  9276  7p7e14  9279  8p4e12  9282  8p6e14  9284  9p4e13  9289  9p5e14  9290  4t4e16  9299  5t4e20  9302  6t4e24  9306  7t4e28  9311  8t4e32  9317  9t4e36  9324  fzo0to42pr  10021  4bc2eq6  10544  ef4p  11424  ef01bndlem  11486  sincosq4sgn  12944
  Copyright terms: Public domain W3C validator