dcn - Intuitionistic Logic Explorer

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

Theorem dcn 842

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

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 629	. . . 4
2	1	orim2i 761	. . 3 $\/$ $\/$
3	2	orcoms 730	. 2 $\/$ $\/$
4		df-dc 835	. 2 DECID $\/$
5		df-dc 835	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 201	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 708 DECID wdc 834

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 614 ax-in2 615 ax-io 709

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

This theorem is referenced by: stdcndc 845 stdcndcOLD 846 dcnn 848 pm5.18dc 883 pm4.67dc 887 pm2.54dc 891 imordc 897 pm4.54dc 902 annimdc 937 pm4.55dc 938 orandc 939 pm3.12dc 958 pm3.13dc 959 dn1dc 960 xor3dc 1387 dfbi3dc 1397 dcned 2353 gcdaddm 11984 prmdc 12129 pcmptdvds 12342

W3C validator