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

Definition df-3 8417
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 8408 . 2  class  3
2 c2 8407 . . 3  class  2
3 c1 7295 . . 3  class  1
4 caddc 7297 . . 3  class  +
52, 3, 4co 5613 . 2  class  ( 2  +  1 )
61, 5wceq 1287 1  wff  3  =  ( 2  +  1 )
Colors of variables: wff set class
This definition is referenced by:  3re  8431  3pos  8451  3m1e2  8476  2p2e4  8477  2p1e3  8483  3p3e6  8492  4p3e7  8494  5p3e8  8497  6p3e9  8500  3t3e9  8507  3nn  8512  2lt3  8520  7p3e10  8883  7p6e13  8886  8p3e11  8889  8p5e13  8891  9p3e12  8896  9p4e13  8897  4t3e12  8906  5t3e15  8909  6t3e18  8913  7t3e21  8918  8t3e24  8924  9t3e27  8931  nn01to3  9034  fztpval  9427  fzo0to42pr  9559  cu2  9951  i3  9954  binom3  9968  fac3  10037  3prm  10992  oddprmge3  10998
  Copyright terms: Public domain W3C validator