dcn - Intuitionistic Logic Explorer

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

Theorem dcn 784

Description: A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.)

**Assertion**
Ref	Expression
dcn	DECID DECID

**Proof of Theorem dcn**
Step	Hyp	Ref	Expression
1		notnot 594	. . . 4
2	1	orim2i 713	. . 3 $\/$ $\/$
3	2	orcoms 684	. 2 $\/$ $\/$
4		df-dc 781	. 2 DECID $\/$
5		df-dc 781	. 2 DECID $\/$
6	3, 4, 5	3imtr4i 199	1 DECID DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 664 DECID wdc 780

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 579 ax-in2 580 ax-io 665

This theorem depends on definitions: df-bi 115 df-dc 781

This theorem is referenced by: pm5.18dc 815 pm4.67dc 819 pm2.54dc 828 imordc 834 pm4.54dc 843 stabtestimpdc 862 annimdc 883 pm4.55dc 884 orandc 885 pm3.12dc 904 pm3.13dc 905 dn1dc 906 xor3dc 1323 dfbi3dc 1333 dcned 2261 gcdaddm 11249