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

Definition df-3 8803
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 8795 . 2 class 3
2 c2 8794 . . 3 class 2
3 c1 7644 . . 3 class 1
4 caddc 7646 . . 3 class +
52, 3, 4co 5781 . 2 class (2 + 1)
61, 5wceq 1332 1 wff 3 = (2 + 1)
Colors of variables: wff set class
This definition is referenced by:  3re  8817  3pos  8837  3m1e2  8863  2p2e4  8870  2p1e3  8876  3p3e6  8885  4p3e7  8887  5p3e8  8890  6p3e9  8893  3t3e9  8900  3nn  8905  2lt3  8913  7p3e10  9279  7p6e13  9282  8p3e11  9285  8p5e13  9287  9p3e12  9292  9p4e13  9293  4t3e12  9302  5t3e15  9305  6t3e18  9309  7t3e21  9314  8t3e24  9320  9t3e27  9327  nn01to3  9435  fztpval  9893  fzo0to42pr  10027  cu2  10421  i3  10424  binom3  10439  fac3  10509  ege2le3  11412  ef4p  11435  cos1bnd  11500  3prm  11843  oddprmge3  11849  dveflem  12893  sincosq3sgn  12955  sincosq4sgn  12956  tangtx  12965  sincos6thpi  12969
  Copyright terms: Public domain W3C validator