dcand - Intuitionistic Logic Explorer

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

Theorem dcand 935

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 837	. . . . 5 DECID $\/$
3		id 19	. . . . . . 7
4	3	intnanrd 934	. . . . . 6 $/\$
5	4	orim2i 763	. . . . 5 $\/$ $\/$ $/\$
6	2, 5	sylbi 121	. . . 4 DECID $\/$ $/\$
7	1, 6	syl 14	. . 3 $\/$ $/\$
8		dcand.2	. . . 4 DECID
9		df-dc 837	. . . . 5 DECID $\/$
10		id 19	. . . . . . 7
11	10	intnand 933	. . . . . 6 $/\$
12	11	orim2i 763	. . . . 5 $\/$ $\/$ $/\$
13	9, 12	sylbi 121	. . . 4 DECID $\/$ $/\$
14	8, 13	syl 14	. . 3 $\/$ $/\$
15		ordir 819	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
16	7, 14, 15	sylanbrc 417	. 2 $/\$ $\/$ $/\$
17		df-dc 837	. 2 DECID $/\$ $/\$ $\/$ $/\$
18	16, 17	sylibr 134	1 DECID $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 710 DECID wdc 836

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 615 ax-in2 616 ax-io 711

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

This theorem is referenced by: dcan 936 dcfi 7098 nn0n0n1ge2b 9472 fzowrddc 11123 bitsinv1 12348 gcdsupex 12353 gcdsupcl 12354 gcdaddm 12380 nnwosdc 12435 lcmval 12460 lcmcllem 12464 lcmledvds 12467 prmdc 12527 pclemdc 12686 infpnlem2 12758 nninfdclemcl 12894