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

Definition df-2 8419
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 8410 . 2  class  2
2 c1 7298 . . 3  class  1
3 caddc 7300 . . 3  class  +
42, 2, 3co 5615 . 2  class  ( 1  +  1 )
51, 4wceq 1287 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  8430  0le2  8450  2pos  8451  1p1e2  8476  2p2e4  8480  2times  8481  3p2e5  8494  4p2e6  8496  5p2e7  8499  6p2e8  8502  7p2e9  8504  2nn  8514  1lt2  8522  nneoor  8784  6p6e12  8885  7p5e12  8888  8p2e10  8891  8p4e12  8893  9p2e11  8898  9p3e12  8899  5t2e10  8911  eluz2b1  9023  nn01to3  9037  fztp  9425  fzprval  9429  fztpval  9430  fzo12sn  9559  rebtwn2zlemstep  9595  rebtwn2z  9597  sqval  9915  fac2  10039  bcp1m1  10073  hashprg  10116  odd2np1lem  10778  opoe  10801  ncoprmgcdne1b  10977  isprm3  11006  prmind2  11008  dvdsnprmd  11013  prmgt1  11019  ex-fl  11122
  Copyright terms: Public domain W3C validator