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

Definition df-4 7975
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 7966 . 2 class 4
2 c3 7965 . . 3 class 3
3 c1 6890 . . 3 class 1
4 caddc 6892 . . 3 class +
52, 3, 4co 5512 . 2 class (3 + 1)
61, 5wceq 1243 1 wff 4 = (3 + 1)
Colors of variables: wff set class
This definition is referenced by:  4re  7992  4pos  8013  2p2e4  8037  3p1e4  8045  3p2e5  8052  4p4e8  8056  5p4e9  8059  6p4e10  8063  4nn  8079  3lt4  8089  halfpm6th  8145  7p4e11  8419  7p7e14  8422  8p4e12  8424  8p6e14  8426  9p4e13  8431  9p5e14  8432  4t4e16  8440  5t4e20  8442  6t4e24  8446  7t4e28  8451  8t4e32  8457  9t4e36  8464  fzo0to42pr  9076
  Copyright terms: Public domain W3C validator