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 7109 nn0n0n1ge2b 9487 fzowrddc 11138 bitsinv1 12388 gcdsupex 12393 gcdsupcl 12394 gcdaddm 12420 nnwosdc 12475 lcmval 12500 lcmcllem 12504 lcmledvds 12507 prmdc 12567 pclemdc 12726 infpnlem2 12798 nninfdclemcl 12934