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

Definition df-2 8049
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 8040 . 2 class 2
2 c1 6948 . . 3 class 1
3 caddc 6950 . . 3 class +
42, 2, 3co 5540 . 2 class (1 + 1)
51, 4wceq 1259 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re  8060  0le2  8080  2pos  8081  1p1e2  8106  2p2e4  8110  2times  8111  3p2e5  8124  4p2e6  8126  5p2e7  8129  6p2e8  8132  7p2e9  8134  2nn  8144  1lt2  8152  nneoor  8399  6p6e12  8500  7p5e12  8503  8p2e10  8506  8p4e12  8508  9p2e11  8513  9p3e12  8514  5t2e10  8526  eluz2b1  8635  nn01to3  8649  fztp  9042  fzprval  9046  fztpval  9047  fzo12sn  9175  rebtwn2zlemstep  9209  rebtwn2z  9211  sqval  9478  fac2  9599  bcp1m1  9633  odd2np1lem  10183  opoe  10207  ex-fl  10279
  Copyright terms: Public domain W3C validator