dcn - Intuitionistic Logic Explorer

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

Theorem dcn 843

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

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 630	. . . 4
2	1	orim2i 762	. . 3 $\/$ $\/$
3	2	orcoms 731	. 2 $\/$ $\/$
4		df-dc 836	. 2 DECID $\/$
5		df-dc 836	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 201	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 709 DECID wdc 835

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710

This theorem depends on definitions: df-bi 117 df-dc 836

This theorem is referenced by: stdcndc 846 stdcndcOLD 847 dcnn 849 pm5.18dc 884 pm4.67dc 888 pm2.54dc 892 imordc 898 pm4.54dc 903 annimdc 939 pm4.55dc 940 orandc 941 pm3.12dc 960 pm3.13dc 961 dn1dc 962 xor3dc 1398 dfbi3dc 1408 dcned 2366 gcdaddm 12003 prmdc 12148 pcmptdvds 12361

W3C validator