dcand - Intuitionistic Logic Explorer

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

Theorem dcand 941

Description: A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) (Revised by BJ, 14-Nov-2024.)

**Hypotheses**
Ref	Expression
dcand.1	DECID
dcand.2	DECID

**Assertion**
Ref	Expression
dcand	DECID $/\$

**Proof of Theorem dcand**
Step	Hyp	Ref	Expression
1		dcand.1	. . . 4 DECID
2		df-dc 843	. . . . 5 DECID $\/$
3		id 19	. . . . . . 7
4	3	intnanrd 940	. . . . . 6 $/\$
5	4	orim2i 769	. . . . 5 $\/$ $\/$ $/\$
6	2, 5	sylbi 121	. . . 4 DECID $\/$ $/\$
7	1, 6	syl 14	. . 3 $\/$ $/\$
8		dcand.2	. . . 4 DECID
9		df-dc 843	. . . . 5 DECID $\/$
10		id 19	. . . . . . 7
11	10	intnand 939	. . . . . 6 $/\$
12	11	orim2i 769	. . . . 5 $\/$ $\/$ $/\$
13	9, 12	sylbi 121	. . . 4 DECID $\/$ $/\$
14	8, 13	syl 14	. . 3 $\/$ $/\$
15		ordir 825	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
16	7, 14, 15	sylanbrc 417	. 2 $/\$ $\/$ $/\$
17		df-dc 843	. 2 DECID $/\$ $/\$ $\/$ $/\$
18	16, 17	sylibr 134	1 DECID $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 716 DECID wdc 842

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 717

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

This theorem is referenced by: dcan 942 dcfi 7281 nn0n0n1ge2b 9675 infssfzcldc 10618 infssfzledc 10619 hashfibclem 11231 fzowrddc 11364 bitsinv1 12673 gcdsupex 12678 gcdsupcl 12679 gcdaddm 12705 nnwosdc 12760 lcmval 12785 lcmcllem 12789 lcmledvds 12792 prmdc 12852 pclemdc 13011 infpnlem2 13083 ballotfilemdifcfi 13169 ballotfilemiex 13188 nninfdclemcl 13283