dcor - Intuitionistic Logic Explorer

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

Theorem dcor 925

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 825	. 2 DECID $\/$
2		orc 702	. . . . . 6 $\/$
3	2	orcd 723	. . . . 5 $\/$ $\/$ $\/$
4		df-dc 825	. . . . 5 DECID $\/$ $\/$ $\/$ $\/$
5	3, 4	sylibr 133	. . . 4 DECID $\/$
6	5	a1d 22	. . 3 DECID DECID $\/$
7		df-dc 825	. . . . 5 DECID $\/$
8		olc 701	. . . . . . . . 9 $\/$
9	8	adantl 275	. . . . . . . 8 $/\$ $\/$
10	9	orcd 723	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
11	10, 4	sylibr 133	. . . . . 6 $/\$ DECID $\/$
12		ioran 742	. . . . . . . . 9 $\/$ $/\$
13	12	biimpri 132	. . . . . . . 8 $/\$ $\/$
14	13	olcd 724	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
15	14, 4	sylibr 133	. . . . . 6 $/\$ DECID $\/$
16	11, 15	jaodan 787	. . . . 5 $/\$ $\/$ DECID $\/$
17	7, 16	sylan2b 285	. . . 4 $/\$ DECID DECID $\/$
18	17	ex 114	. . 3 DECID DECID $\/$
19	6, 18	jaoi 706	. 2 $\/$ DECID DECID $\/$
20	1, 19	sylbi 120	1 DECID DECID DECID $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103 $\/$ wo 698 DECID wdc 824

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699

This theorem depends on definitions: df-bi 116 df-dc 825

This theorem is referenced by: pm4.55dc 928 orandc 929 pm3.12dc 948 pm3.13dc 949 dn1dc 950 eueq3dc 2900 distrlem4prl 7525 distrlem4pru 7526 exfzdc 10175 lcmmndc 11994 isprm3 12050 lgsval 13545 lgsfvalg 13546 lgsfcl2 13547 lgsval2lem 13551 lgsdir2 13574 lgsne0 13579 lgsdirnn0 13588 lgsdinn0 13589