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

Definition df-2 8736
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 8728 . 2 class 2
2 c1 7585 . . 3 class 1
3 caddc 7587 . . 3 class +
42, 2, 3co 5740 . 2 class (1 + 1)
51, 4wceq 1314 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re  8747  0le2  8767  2pos  8768  1p1e2  8794  2p2e4  8798  2times  8799  3p2e5  8812  4p2e6  8814  5p2e7  8817  6p2e8  8820  7p2e9  8822  2nn  8832  1lt2  8840  nneoor  9104  6p6e12  9206  7p5e12  9209  8p2e10  9212  8p4e12  9214  9p2e11  9219  9p3e12  9220  5t2e10  9232  eluz2b1  9344  nn01to3  9358  fztp  9798  fzprval  9802  fztpval  9803  fzo12sn  9934  rebtwn2zlemstep  9970  rebtwn2z  9972  sqval  10291  fac2  10417  bcp1m1  10451  hashprg  10494  binom11  11195  ege2le3  11276  ef4p  11299  efgt1p2  11300  eirraplem  11379  odd2np1lem  11465  opoe  11488  ncoprmgcdne1b  11666  isprm3  11695  prmind2  11697  dvdsnprmd  11702  prmgt1  11708  dveflem  12738  ex-fl  12748
  Copyright terms: Public domain W3C validator