![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-2 | Unicode version |
Description: Define the number 2. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2 8571 |
. 2
![]() ![]() | |
2 | c1 7448 |
. . 3
![]() ![]() | |
3 | caddc 7450 |
. . 3
![]() ![]() | |
4 | 2, 2, 3 | co 5690 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | wceq 1296 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 2re 8590 0le2 8610 2pos 8611 1p1e2 8637 2p2e4 8641 2times 8642 3p2e5 8655 4p2e6 8657 5p2e7 8660 6p2e8 8663 7p2e9 8665 2nn 8675 1lt2 8683 nneoor 8947 6p6e12 9049 7p5e12 9052 8p2e10 9055 8p4e12 9057 9p2e11 9062 9p3e12 9063 5t2e10 9075 eluz2b1 9187 nn01to3 9201 fztp 9641 fzprval 9645 fztpval 9646 fzo12sn 9777 rebtwn2zlemstep 9813 rebtwn2z 9815 sqval 10128 fac2 10254 bcp1m1 10288 hashprg 10331 binom11 11029 ege2le3 11110 ef4p 11133 efgt1p2 11134 eirraplem 11213 odd2np1lem 11299 opoe 11322 ncoprmgcdne1b 11498 isprm3 11527 prmind2 11529 dvdsnprmd 11534 prmgt1 11540 ex-fl 12360 |
Copyright terms: Public domain | W3C validator |