dcn - Intuitionistic Logic Explorer

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

Theorem dcn 828

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

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 619	. . . 4
2	1	orim2i 751	. . 3 $\/$ $\/$
3	2	orcoms 720	. 2 $\/$ $\/$
4		df-dc 821	. 2 DECID $\/$
5		df-dc 821	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 200	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 698 DECID wdc 820

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 604 ax-in2 605 ax-io 699

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

This theorem is referenced by: stdcndc 831 stdcndcOLD 832 dcnn 834 pm5.18dc 869 pm4.67dc 873 pm2.54dc 877 imordc 883 pm4.54dc 888 annimdc 922 pm4.55dc 923 orandc 924 pm3.12dc 943 pm3.13dc 944 dn1dc 945 xor3dc 1369 dfbi3dc 1379 dcned 2333 gcdaddm 11884 prmdc 12023

W3C validator