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

Definition df-3 8744
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 8736 . 2  class  3
2 c2 8735 . . 3  class  2
3 c1 7589 . . 3  class  1
4 caddc 7591 . . 3  class  +
52, 3, 4co 5742 . 2  class  ( 2  +  1 )
61, 5wceq 1316 1  wff  3  =  ( 2  +  1 )
Colors of variables: wff set class
This definition is referenced by:  3re  8758  3pos  8778  3m1e2  8804  2p2e4  8805  2p1e3  8811  3p3e6  8820  4p3e7  8822  5p3e8  8825  6p3e9  8828  3t3e9  8835  3nn  8840  2lt3  8848  7p3e10  9214  7p6e13  9217  8p3e11  9220  8p5e13  9222  9p3e12  9227  9p4e13  9228  4t3e12  9237  5t3e15  9240  6t3e18  9244  7t3e21  9249  8t3e24  9255  9t3e27  9262  nn01to3  9365  fztpval  9818  fzo0to42pr  9952  cu2  10346  i3  10349  binom3  10364  fac3  10433  ege2le3  11291  ef4p  11314  cos1bnd  11380  3prm  11721  oddprmge3  11727  dveflem  12766  sincosq3sgn  12820  sincosq4sgn  12821
  Copyright terms: Public domain W3C validator