dcor - Intuitionistic Logic Explorer

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

Theorem dcor 930

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 830	. 2 DECID $\/$
2		orc 707	. . . . . 6 $\/$
3	2	orcd 728	. . . . 5 $\/$ $\/$ $\/$
4		df-dc 830	. . . . 5 DECID $\/$ $\/$ $\/$ $\/$
5	3, 4	sylibr 133	. . . 4 DECID $\/$
6	5	a1d 22	. . 3 DECID DECID $\/$
7		df-dc 830	. . . . 5 DECID $\/$
8		olc 706	. . . . . . . . 9 $\/$
9	8	adantl 275	. . . . . . . 8 $/\$ $\/$
10	9	orcd 728	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
11	10, 4	sylibr 133	. . . . . 6 $/\$ DECID $\/$
12		ioran 747	. . . . . . . . 9 $\/$ $/\$
13	12	biimpri 132	. . . . . . . 8 $/\$ $\/$
14	13	olcd 729	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
15	14, 4	sylibr 133	. . . . . 6 $/\$ DECID $\/$
16	11, 15	jaodan 792	. . . . 5 $/\$ $\/$ DECID $\/$
17	7, 16	sylan2b 285	. . . 4 $/\$ DECID DECID $\/$
18	17	ex 114	. . 3 DECID DECID $\/$
19	6, 18	jaoi 711	. 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 703 DECID wdc 829

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 609 ax-in2 610 ax-io 704

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

This theorem is referenced by: pm4.55dc 933 orandc 934 pm3.12dc 953 pm3.13dc 954 dn1dc 955 eueq3dc 2904 distrlem4prl 7546 distrlem4pru 7547 exfzdc 10196 lcmmndc 12016 isprm3 12072 lgsval 13699 lgsfvalg 13700 lgsfcl2 13701 lgsval2lem 13705 lgsdir2 13728 lgsne0 13733 lgsdirnn0 13742 lgsdinn0 13743