![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-2 | GIF version |
Description: Define the number 2. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-2 | ⊢ 2 = (1 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2 8534 | . 2 class 2 | |
2 | c1 7412 | . . 3 class 1 | |
3 | caddc 7414 | . . 3 class + | |
4 | 2, 2, 3 | co 5666 | . 2 class (1 + 1) |
5 | 1, 4 | wceq 1290 | 1 wff 2 = (1 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 2re 8553 0le2 8573 2pos 8574 1p1e2 8600 2p2e4 8604 2times 8605 3p2e5 8618 4p2e6 8620 5p2e7 8623 6p2e8 8626 7p2e9 8628 2nn 8638 1lt2 8646 nneoor 8909 6p6e12 9011 7p5e12 9014 8p2e10 9017 8p4e12 9019 9p2e11 9024 9p3e12 9025 5t2e10 9037 eluz2b1 9149 nn01to3 9163 fztp 9553 fzprval 9557 fztpval 9558 fzo12sn 9689 rebtwn2zlemstep 9725 rebtwn2z 9727 sqval 10074 fac2 10200 bcp1m1 10234 hashprg 10277 binom11 10941 ege2le3 11022 ef4p 11045 efgt1p2 11046 eirraplem 11125 odd2np1lem 11211 opoe 11234 ncoprmgcdne1b 11410 isprm3 11439 prmind2 11441 dvdsnprmd 11446 prmgt1 11452 ex-fl 11925 |
Copyright terms: Public domain | W3C validator |