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 2994 distrlem4prl 7915 distrlem4pru 7916 exfzdc 10608 lcmmndc 12784 isprm3 12840 perfectlem2 15994 lgsval 16003 lgsfvalg 16004 lgsfcl2 16005 lgsval2lem 16009 lgsdir2 16032 lgsne0 16037 lgsdirnn0 16046 lgsdinn0 16047 2lgs 16103 2lgsoddprm 16112 eupth2lem3lem4fi 16594 eupth2lem3lem7fi 16595 cndcap 16970