dcn - Intuitionistic Logic Explorer

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

Theorem dcn 850

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

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 634	. . . 4
2	1	orim2i 769	. . 3 $\/$ $\/$
3	2	orcoms 738	. 2 $\/$ $\/$
4		df-dc 843	. 2 DECID $\/$
5		df-dc 843	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 201	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 716 DECID wdc 842

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 619 ax-in2 620 ax-io 717

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

This theorem is referenced by: stdcndc 853 stdcndcOLD 854 dcnn 856 pm5.18dc 891 pm4.67dc 895 pm2.54dc 899 imordc 905 pm4.54dc 910 annimdc 946 pm4.55dc 947 orandc 948 pm3.12dc 967 pm3.13dc 968 dn1dc 969 ifpnst 997 xor3dc 1432 dfbi3dc 1442 dcned 2409 qdcle 10569 bitsdc 12588 gcdaddm 12635 prmdc 12782 pcmptdvds 12998 lgsquadlemofi 15895 konigsberglem5 16433

W3C validator