dcor - Intuitionistic Logic Explorer

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

Theorem dcor 941

Description: A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)

**Assertion**
Ref	Expression
dcor	DECID DECID DECID $\/$

**Proof of Theorem dcor**
Step	Hyp	Ref	Expression
1		df-dc 840	. 2 DECID $\/$
2		orc 717	. . . . . 6 $\/$
3	2	orcd 738	. . . . 5 $\/$ $\/$ $\/$
4		df-dc 840	. . . . 5 DECID $\/$ $\/$ $\/$ $\/$
5	3, 4	sylibr 134	. . . 4 DECID $\/$
6	5	a1d 22	. . 3 DECID DECID $\/$
7		df-dc 840	. . . . 5 DECID $\/$
8		olc 716	. . . . . . . . 9 $\/$
9	8	adantl 277	. . . . . . . 8 $/\$ $\/$
10	9	orcd 738	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
11	10, 4	sylibr 134	. . . . . 6 $/\$ DECID $\/$
12		ioran 757	. . . . . . . . 9 $\/$ $/\$
13	12	biimpri 133	. . . . . . . 8 $/\$ $\/$
14	13	olcd 739	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
15	14, 4	sylibr 134	. . . . . 6 $/\$ DECID $\/$
16	11, 15	jaodan 802	. . . . 5 $/\$ $\/$ DECID $\/$
17	7, 16	sylan2b 287	. . . 4 $/\$ DECID DECID $\/$
18	17	ex 115	. . 3 DECID DECID $\/$
19	6, 18	jaoi 721	. 2 $\/$ DECID DECID $\/$
20	1, 19	sylbi 121	1 DECID DECID DECID $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 713 DECID wdc 839

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 617 ax-in2 618 ax-io 714

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

This theorem is referenced by: pm4.55dc 944 orandc 945 pm3.12dc 964 pm3.13dc 965 dn1dc 966 eueq3dc 2977 distrlem4prl 7782 distrlem4pru 7783 exfzdc 10458 lcmmndc 12599 isprm3 12655 perfectlem2 15689 lgsval 15698 lgsfvalg 15699 lgsfcl2 15700 lgsval2lem 15704 lgsdir2 15727 lgsne0 15732 lgsdirnn0 15741 lgsdinn0 15742 2lgs 15798 2lgsoddprm 15807 cndcap 16487