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 7804 distrlem4pru 7805 exfzdc 10487 lcmmndc 12652 isprm3 12708 perfectlem2 15743 lgsval 15752 lgsfvalg 15753 lgsfcl2 15754 lgsval2lem 15758 lgsdir2 15781 lgsne0 15786 lgsdirnn0 15795 lgsdinn0 15796 2lgs 15852 2lgsoddprm 15861 eupth2lem3lem4fi 16343 eupth2lem3lem7fi 16344 cndcap 16715