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 10698 hashfibclem 11304 bitsdc 12739 gcdaddm 12786 prmdc 12933 pcmptdvds 13153 ballotfilemdifcfi 13283 ballotfilemdifcfz 13285 ballotfilem2 13286 ballotfilembfi 13297 bposlem6 16316 lgsquadlemofi 16400 konigsberglem5 16938

W3C validator