dcn - Intuitionistic Logic Explorer

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

Theorem dcn 832

Description: The negation of a decidable proposition is decidable. The converse need not hold, but does hold for negated propositions, see dcnn 838. (Contributed by Jim Kingdon, 25-Mar-2018.)

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 619	. . . 4
2	1	orim2i 751	. . 3 $\/$ $\/$
3	2	orcoms 720	. 2 $\/$ $\/$
4		df-dc 825	. 2 DECID $\/$
5		df-dc 825	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 200	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 698 DECID wdc 824

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 604 ax-in2 605 ax-io 699

This theorem depends on definitions: df-bi 116 df-dc 825

This theorem is referenced by: stdcndc 835 stdcndcOLD 836 dcnn 838 pm5.18dc 873 pm4.67dc 877 pm2.54dc 881 imordc 887 pm4.54dc 892 annimdc 927 pm4.55dc 928 orandc 929 pm3.12dc 948 pm3.13dc 949 dn1dc 950 xor3dc 1377 dfbi3dc 1387 dcned 2342 gcdaddm 11917 prmdc 12062 pcmptdvds 12275

W3C validator