dcn - Intuitionistic Logic Explorer

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

Theorem dcn 844

Description: The negation of a decidable proposition is decidable. The converse need not hold, but does hold for negated propositions, see dcnn 850. (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 763	. . 3 $\/$ $\/$
3	2	orcoms 732	. 2 $\/$ $\/$
4		df-dc 837	. 2 DECID $\/$
5		df-dc 837	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 201	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 710 DECID wdc 836

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 711

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

This theorem is referenced by: stdcndc 847 stdcndcOLD 848 dcnn 850 pm5.18dc 885 pm4.67dc 889 pm2.54dc 893 imordc 899 pm4.54dc 904 annimdc 940 pm4.55dc 941 orandc 942 pm3.12dc 961 pm3.13dc 962 dn1dc 963 xor3dc 1407 dfbi3dc 1417 dcned 2382 qdcle 10389 bitsdc 12258 gcdaddm 12305 prmdc 12452 pcmptdvds 12668 lgsquadlemofi 15553

W3C validator