dcn - Intuitionistic Logic Explorer

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

Theorem dcn 827

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

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 618	. . . 4
2	1	orim2i 750	. . 3 $\/$ $\/$
3	2	orcoms 719	. 2 $\/$ $\/$
4		df-dc 820	. 2 DECID $\/$
5		df-dc 820	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 200	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 697 DECID wdc 819

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 603 ax-in2 604 ax-io 698

This theorem depends on definitions: df-bi 116 df-dc 820

This theorem is referenced by: stdcndc 830 stdcndcOLD 831 dcnn 833 pm5.18dc 868 pm4.67dc 872 pm2.54dc 876 imordc 882 pm4.54dc 887 annimdc 921 pm4.55dc 922 orandc 923 pm3.12dc 942 pm3.13dc 943 dn1dc 944 xor3dc 1365 dfbi3dc 1375 dcned 2314 gcdaddm 11672

W3C validator