dcor - Intuitionistic Logic Explorer

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

Theorem dcor 948

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 847	. 2 DECID $\/$
2		orc 724	. . . . . 6 $\/$
3	2	orcd 745	. . . . 5 $\/$ $\/$ $\/$
4		df-dc 847	. . . . 5 DECID $\/$ $\/$ $\/$ $\/$
5	3, 4	sylibr 134	. . . 4 DECID $\/$
6	5	a1d 22	. . 3 DECID DECID $\/$
7		df-dc 847	. . . . 5 DECID $\/$
8		olc 723	. . . . . . . . 9 $\/$
9	8	adantl 277	. . . . . . . 8 $/\$ $\/$
10	9	orcd 745	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
11	10, 4	sylibr 134	. . . . . 6 $/\$ DECID $\/$
12		ioran 764	. . . . . . . . 9 $\/$ $/\$
13	12	biimpri 133	. . . . . . . 8 $/\$ $\/$
14	13	olcd 746	. . . . . . 7 $/\$ $\/$ $\/$ $\/$
15	14, 4	sylibr 134	. . . . . 6 $/\$ DECID $\/$
16	11, 15	jaodan 809	. . . . 5 $/\$ $\/$ DECID $\/$
17	7, 16	sylan2b 287	. . . 4 $/\$ DECID DECID $\/$
18	17	ex 115	. . 3 DECID DECID $\/$
19	6, 18	jaoi 728	. 2 $\/$ DECID DECID $\/$
20	1, 19	sylbi 121	1 DECID DECID DECID $\/$

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 720 DECID wdc 846

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721

This proof depends on definitions: df-bi 117 df-dc 847

This theorem is used by: pm4.55dc 951 orandc 952 pm3.12dc 971 pm3.13dc 972 dn1dc 973 eueq3dc 3000 distrlem4prl 7952 distrlem4pru 7953 exfzdc 10670 lcmmndc 12859 isprm3 12915 ppiqub 16254 perfectlem2 16261 lgsval 16289 lgsfvalg 16290 lgsfcl2 16291 lgsval2lem 16295 lgsdir2 16318 lgsne0 16323 lgsdirnn0 16332 lgsdinn0 16333 2lgs 16389 2lgsoddprm 16398 eupth2lem3lem4fi 16880 eupth2lem3lem7fi 16881 cndcap 17276