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

Definition df-2 7753
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 7744 . 2  2
2 c1 6712 . . 3  1
3 caddc 6714 . . 3  +
42, 2, 3co 5455 . 2  1  +  1
51, 4wceq 1242 1  2  1  +  1
Colors of variables: wff set class
This definition is referenced by:  2re  7765  0le2  7786  2pos  7787  1p1e2  7811  2p2e4  7815  2times  7816  3p2e5  7830  4p2e6  7832  5p2e7  7835  6p2e8  7839  7p2e9  7842  8p2e10  7844  2nn  7855  1lt2  7864  nneoor  8116  6p6e12  8194  7p5e12  8196  8p4e12  8200  9p2e11  8205  9p3e12  8206  eluz2b1  8315  nn01to3  8328  fztp  8710  fzprval  8714  fztpval  8715  fzo12sn  8843  sqval  8966
  Copyright terms: Public domain W3C validator