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

Definition df-4 8421
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 8412 . 2 class 4
2 c3 8411 . . 3 class 3
3 c1 7298 . . 3 class 1
4 caddc 7300 . . 3 class +
52, 3, 4co 5615 . 2 class (3 + 1)
61, 5wceq 1287 1 wff 4 = (3 + 1)
Colors of variables: wff set class
This definition is referenced by:  4re  8437  4pos  8457  2p2e4  8480  3p1e4  8488  3p2e5  8494  4p4e8  8498  5p4e9  8501  4nn  8516  3lt4  8525  halfpm6th  8572  6p4e10  8883  7p4e11  8887  7p7e14  8890  8p4e12  8893  8p6e14  8895  9p4e13  8900  9p5e14  8901  4t4e16  8910  5t4e20  8913  6t4e24  8917  7t4e28  8922  8t4e32  8928  9t4e36  8935  fzo0to42pr  9562  4bc2eq6  10082
  Copyright terms: Public domain W3C validator