dcor - Intuitionistic Logic Explorer

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

Theorem dcor 938

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

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 711

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

This theorem is referenced by: pm4.55dc 941 orandc 942 pm3.12dc 961 pm3.13dc 962 dn1dc 963 eueq3dc 2951 distrlem4prl 7717 distrlem4pru 7718 exfzdc 10391 lcmmndc 12459 isprm3 12515 perfectlem2 15547 lgsval 15556 lgsfvalg 15557 lgsfcl2 15558 lgsval2lem 15562 lgsdir2 15585 lgsne0 15590 lgsdirnn0 15599 lgsdinn0 15600 2lgs 15656 2lgsoddprm 15665 cndcap 16139