dcn - Intuitionistic Logic Explorer

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

Theorem dcn 837

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.)

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
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

W3C validator