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

Definition df-2 8743
Description: Define the number 2. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-2  |-  2  =  ( 1  +  1 )

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 8735 . 2  class  2
2 c1 7589 . . 3  class  1
3 caddc 7591 . . 3  class  +
42, 2, 3co 5742 . 2  class  ( 1  +  1 )
51, 4wceq 1316 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  8754  0le2  8774  2pos  8775  1p1e2  8801  2p2e4  8805  2times  8806  3p2e5  8819  4p2e6  8821  5p2e7  8824  6p2e8  8827  7p2e9  8829  2nn  8839  1lt2  8847  nneoor  9111  6p6e12  9213  7p5e12  9216  8p2e10  9219  8p4e12  9221  9p2e11  9226  9p3e12  9227  5t2e10  9239  eluz2b1  9351  nn01to3  9365  fztp  9813  fzprval  9817  fztpval  9818  fzo12sn  9949  rebtwn2zlemstep  9985  rebtwn2z  9987  sqval  10306  fac2  10432  bcp1m1  10466  hashprg  10509  binom11  11210  ege2le3  11291  ef4p  11314  efgt1p2  11315  eirraplem  11395  odd2np1lem  11481  opoe  11504  ncoprmgcdne1b  11682  isprm3  11711  prmind2  11713  dvdsnprmd  11718  prmgt1  11724  dveflem  12766  ex-fl  12833
  Copyright terms: Public domain W3C validator