dcor - Intuitionistic Logic Explorer

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

Theorem dcor 944

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 843	. 2 DECID $\/$
2		orc 720	. . . . . 6 $\/$
3	2	orcd 741	. . . . 5 $\/$ $\/$ $\/$
4		df-dc 843	. . . . 5 DECID $\/$ $\/$ $\/$ $\/$
5	3, 4	sylibr 134	. . . 4 DECID $\/$
6	5	a1d 22	. . 3 DECID DECID $\/$
7		df-dc 843	. . . . 5 DECID $\/$
8		olc 719	. . . . . . . . 9 $\/$
9	8	adantl 277	. . . . . . . 8 $/\$ $\/$
10	9	orcd 741	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
11	10, 4	sylibr 134	. . . . . 6 $/\$ DECID $\/$
12		ioran 760	. . . . . . . . 9 $\/$ $/\$
13	12	biimpri 133	. . . . . . . 8 $/\$ $\/$
14	13	olcd 742	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
15	14, 4	sylibr 134	. . . . . 6 $/\$ DECID $\/$
16	11, 15	jaodan 805	. . . . 5 $/\$ $\/$ DECID $\/$
17	7, 16	sylan2b 287	. . . 4 $/\$ DECID DECID $\/$
18	17	ex 115	. . 3 DECID DECID $\/$
19	6, 18	jaoi 724	. 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 716 DECID wdc 842

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 619 ax-in2 620 ax-io 717

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

This theorem is referenced by: pm4.55dc 947 orandc 948 pm3.12dc 967 pm3.13dc 968 dn1dc 969 eueq3dc 2991 distrlem4prl 7899 distrlem4pru 7900 exfzdc 10586 lcmmndc 12759 isprm3 12815 perfectlem2 15868 lgsval 15877 lgsfvalg 15878 lgsfcl2 15879 lgsval2lem 15883 lgsdir2 15906 lgsne0 15911 lgsdirnn0 15920 lgsdinn0 15921 2lgs 15977 2lgsoddprm 15986 eupth2lem3lem4fi 16468 eupth2lem3lem7fi 16469 cndcap 16844