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

Definition df-3 7974
Description: Define the number 3. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-3 3 = (2 + 1)

Detailed syntax breakdown of Definition df-3
StepHypRef Expression
1 c3 7965 . 2 class 3
2 c2 7964 . . 3 class 2
3 c1 6890 . . 3 class 1
4 caddc 6892 . . 3 class +
52, 3, 4co 5512 . 2 class (2 + 1)
61, 5wceq 1243 1 wff 3 = (2 + 1)
Colors of variables: wff set class
This definition is referenced by:  3re  7989  3pos  8010  3m1e2  8036  2p2e4  8037  2p1e3  8043  3p3e6  8053  4p3e7  8055  5p3e8  8058  6p3e9  8062  7p3e10  8065  3t3e9  8072  3nn  8078  2lt3  8087  7p6e13  8421  8p3e11  8423  8p5e13  8425  9p3e12  8430  9p4e13  8431  4t3e12  8439  5t3e15  8441  6t3e18  8445  7t3e21  8450  8t3e24  8456  9t3e27  8463  nn01to3  8552  fztpval  8945  fzo0to42pr  9076  cu2  9351  i3  9354  binom3  9366
  Copyright terms: Public domain W3C validator