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

Definition df-3 8166
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 8157 . 2 class 3
2 c2 8156 . . 3 class 2
3 c1 7044 . . 3 class 1
4 caddc 7046 . . 3 class +
52, 3, 4co 5543 . 2 class (2 + 1)
61, 5wceq 1285 1 wff 3 = (2 + 1)
Colors of variables: wff set class
This definition is referenced by:  3re  8180  3pos  8200  3m1e2  8225  2p2e4  8226  2p1e3  8232  3p3e6  8241  4p3e7  8243  5p3e8  8246  6p3e9  8249  3t3e9  8256  3nn  8261  2lt3  8269  7p3e10  8632  7p6e13  8635  8p3e11  8638  8p5e13  8640  9p3e12  8645  9p4e13  8646  4t3e12  8655  5t3e15  8658  6t3e18  8662  7t3e21  8667  8t3e24  8673  9t3e27  8680  nn01to3  8783  fztpval  9176  fzo0to42pr  9306  cu2  9670  i3  9673  binom3  9687  fac3  9756  3prm  10654  oddprmge3  10660
  Copyright terms: Public domain W3C validator