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

Definition df-2 7733
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 7724 . 2 class 2
2 c1 6692 . . 3 class 1
3 caddc 6694 . . 3 class +
42, 2, 3co 5455 . 2 class (1 + 1)
51, 4wceq 1242 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re  7745  0le2  7766  2pos  7767  1p1e2  7791  2p2e4  7795  2times  7796  3p2e5  7810  4p2e6  7812  5p2e7  7815  6p2e8  7819  7p2e9  7822  8p2e10  7824  2nn  7835  1lt2  7844  nneoor  8096  6p6e12  8174  7p5e12  8176  8p4e12  8180  9p2e11  8185  9p3e12  8186  eluz2b1  8295  nn01to3  8308  fztp  8690  fzprval  8694  fztpval  8695  fzo12sn  8823  sqval  8946
  Copyright terms: Public domain W3C validator