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 7767 distrlem4pru 7768 exfzdc 10441 lcmmndc 12579 isprm3 12635 perfectlem2 15668 lgsval 15677 lgsfvalg 15678 lgsfcl2 15679 lgsval2lem 15683 lgsdir2 15706 lgsne0 15711 lgsdirnn0 15720 lgsdinn0 15721 2lgs 15777 2lgsoddprm 15786 cndcap 16386