dcn - Intuitionistic Logic Explorer

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

Theorem dcn 847

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

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 632	. . . 4
2	1	orim2i 766	. . 3 $\/$ $\/$
3	2	orcoms 735	. 2 $\/$ $\/$
4		df-dc 840	. 2 DECID $\/$
5		df-dc 840	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 201	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 713 DECID wdc 839

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 617 ax-in2 618 ax-io 714

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

This theorem is referenced by: stdcndc 850 stdcndcOLD 851 dcnn 853 pm5.18dc 888 pm4.67dc 892 pm2.54dc 896 imordc 902 pm4.54dc 907 annimdc 943 pm4.55dc 944 orandc 945 pm3.12dc 964 pm3.13dc 965 dn1dc 966 ifpnst 994 xor3dc 1429 dfbi3dc 1439 dcned 2406 qdcle 10466 bitsdc 12458 gcdaddm 12505 prmdc 12652 pcmptdvds 12868 lgsquadlemofi 15755

W3C validator