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

Definition df-3 7734
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 7725 . 2 class 3
2 c2 7724 . . 3 class 2
3 c1 6692 . . 3 class 1
4 caddc 6694 . . 3 class +
52, 3, 4co 5455 . 2 class (2 + 1)
61, 5wceq 1242 1 wff 3 = (2 + 1)
Colors of variables: wff set class
This definition is referenced by:  3re  7749  3pos  7770  3m1e2  7794  2p2e4  7795  2p1e3  7801  3p3e6  7811  4p3e7  7813  5p3e8  7816  6p3e9  7820  7p3e10  7823  3t3e9  7830  3nn  7836  2lt3  7845  7p6e13  8177  8p3e11  8179  8p5e13  8181  9p3e12  8186  9p4e13  8187  4t3e12  8195  5t3e15  8197  6t3e18  8201  7t3e21  8206  8t3e24  8212  9t3e27  8219  nn01to3  8308  fztpval  8695  fzo0to42pr  8826  cu2  8984  i3  8987  binom3  8999
  Copyright terms: Public domain W3C validator