Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dcn | Unicode version |
Description: The negation of a decidable proposition is decidable. The converse need not hold, but does hold for negated propositions, see dcnn 843. (Contributed by Jim Kingdon, 25-Mar-2018.) |
Ref | Expression |
---|---|
dcn | DECID DECID |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot 624 | . . . 4 | |
2 | 1 | orim2i 756 | . . 3 |
3 | 2 | orcoms 725 | . 2 |
4 | df-dc 830 | . 2 DECID | |
5 | df-dc 830 | . 2 DECID | |
6 | 3, 4, 5 | 3imtr4i 200 | 1 DECID DECID |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wo 703 DECID wdc 829 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 |
This theorem depends on definitions: df-bi 116 df-dc 830 |
This theorem is referenced by: stdcndc 840 stdcndcOLD 841 dcnn 843 pm5.18dc 878 pm4.67dc 882 pm2.54dc 886 imordc 892 pm4.54dc 897 annimdc 932 pm4.55dc 933 orandc 934 pm3.12dc 953 pm3.13dc 954 dn1dc 955 xor3dc 1382 dfbi3dc 1392 dcned 2346 gcdaddm 11939 prmdc 12084 pcmptdvds 12297 |
Copyright terms: Public domain | W3C validator |