dcn - Intuitionistic Logic Explorer

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

Theorem dcn 854

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

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 638	. . . 4
2	1	orim2i 773	. . 3 $\/$ $\/$
3	2	orcoms 742	. 2 $\/$ $\/$
4		df-dc 847	. 2 DECID $\/$
5		df-dc 847	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 201	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 720 DECID wdc 846

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 623 ax-in2 624 ax-io 721

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

This theorem is referenced by: stdcndc 857 stdcndcOLD 858 dcnn 860 pm5.18dc 895 pm4.67dc 899 pm2.54dc 903 imordc 909 pm4.54dc 914 annimdc 950 pm4.55dc 951 orandc 952 pm3.12dc 971 pm3.13dc 972 dn1dc 973 ifpnst 1001 xor3dc 1436 dfbi3dc 1446 dcned 2426 qdcle 10659 hashfibclem 11260 bitsdc 12692 gcdaddm 12739 prmdc 12886 pcmptdvds 13102 ballotfilemdifcfi 13203 ballotfilemdifcfz 13205 ballotfilem2 13206 ballotfilembfi 13217 lgsquadlemofi 16109 konigsberglem5 16647

W3C validator