dcor - Intuitionistic Logic Explorer

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

Theorem dcor 937

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 836	. 2 DECID $\/$
2		orc 713	. . . . . 6 $\/$
3	2	orcd 734	. . . . 5 $\/$ $\/$ $\/$
4		df-dc 836	. . . . 5 DECID $\/$ $\/$ $\/$ $\/$
5	3, 4	sylibr 134	. . . 4 DECID $\/$
6	5	a1d 22	. . 3 DECID DECID $\/$
7		df-dc 836	. . . . 5 DECID $\/$
8		olc 712	. . . . . . . . 9 $\/$
9	8	adantl 277	. . . . . . . 8 $/\$ $\/$
10	9	orcd 734	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
11	10, 4	sylibr 134	. . . . . 6 $/\$ DECID $\/$
12		ioran 753	. . . . . . . . 9 $\/$ $/\$
13	12	biimpri 133	. . . . . . . 8 $/\$ $\/$
14	13	olcd 735	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
15	14, 4	sylibr 134	. . . . . 6 $/\$ DECID $\/$
16	11, 15	jaodan 798	. . . . 5 $/\$ $\/$ DECID $\/$
17	7, 16	sylan2b 287	. . . 4 $/\$ DECID DECID $\/$
18	17	ex 115	. . 3 DECID DECID $\/$
19	6, 18	jaoi 717	. 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 709 DECID wdc 835

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 615 ax-in2 616 ax-io 710

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

This theorem is referenced by: pm4.55dc 940 orandc 941 pm3.12dc 960 pm3.13dc 961 dn1dc 962 eueq3dc 2946 distrlem4prl 7679 distrlem4pru 7680 exfzdc 10350 lcmmndc 12303 isprm3 12359 perfectlem2 15390 lgsval 15399 lgsfvalg 15400 lgsfcl2 15401 lgsval2lem 15405 lgsdir2 15428 lgsne0 15433 lgsdirnn0 15442 lgsdinn0 15443 2lgs 15499 2lgsoddprm 15508 cndcap 15862