dcor - Intuitionistic Logic Explorer

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

Theorem dcor 943

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

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 716

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

This theorem is referenced by: pm4.55dc 946 orandc 947 pm3.12dc 966 pm3.13dc 967 dn1dc 968 eueq3dc 2980 distrlem4prl 7803 distrlem4pru 7804 exfzdc 10485 lcmmndc 12633 isprm3 12689 perfectlem2 15723 lgsval 15732 lgsfvalg 15733 lgsfcl2 15734 lgsval2lem 15738 lgsdir2 15761 lgsne0 15766 lgsdirnn0 15775 lgsdinn0 15776 2lgs 15832 2lgsoddprm 15841 cndcap 16663