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

This proof depends on syntax axioms:

wn 3

wi 4 $\/$ wo 720 DECID wdc 846

This proof depends on 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 proof depends on definitions: df-bi 117 df-dc 847

This theorem is used 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 10697 hashfibclem 11303 bitsdc 12738 gcdaddm 12785 prmdc 12932 pcmptdvds 13152 ballotfilemdifcfi 13282 ballotfilemdifcfz 13284 ballotfilem2 13285 ballotfilembfi 13296 bposlem6 16333 lgsquadlemofi 16417 konigsberglem5 16955

W3C validator