dcand - Intuitionistic Logic Explorer

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

Theorem dcand 945

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 847	. . . . 5 DECID $\/$
3		id 19	. . . . . . 7
4	3	intnanrd 944	. . . . . 6 $/\$
5	4	orim2i 773	. . . . 5 $\/$ $\/$ $/\$
6	2, 5	sylbi 121	. . . 4 DECID $\/$ $/\$
7	1, 6	syl 14	. . 3 $\/$ $/\$
8		dcand.2	. . . 4 DECID
9		df-dc 847	. . . . 5 DECID $\/$
10		id 19	. . . . . . 7
11	10	intnand 943	. . . . . 6 $/\$
12	11	orim2i 773	. . . . 5 $\/$ $\/$ $/\$
13	9, 12	sylbi 121	. . . 4 DECID $\/$ $/\$
14	8, 13	syl 14	. . 3 $\/$ $/\$
15		ordir 829	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
16	7, 14, 15	sylanbrc 421	. 2 $/\$ $\/$ $/\$
17		df-dc 847	. 2 DECID $/\$ $/\$ $\/$ $/\$
18	16, 17	sylibr 134	1 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: dcan 946 dcfi 7320 fdcf1 7321 nn0n0n1ge2b 9736 infssfzcldc 10686 infssfzledc 10687 hashfibclem 11304 fzowrddc 11441 bitsinv1 12754 gcdsupex 12759 gcdsupcl 12760 gcdaddm 12786 nnwosdc 12841 lcmval 12866 lcmcllem 12870 lcmledvds 12873 prmdc 12933 pclemdc 13096 infpnlem2 13168 ballotfilemdifcfi 13283 ballotfilemiex 13302 nninfdclemcl 13397 gsummptfidmsplit 14254 ppiqfi 16242 prmdvdsfi 16243 ppiprm 16259 chtprm 16261 chtdif 16264 efchtqdvds 16265 ppidif 16269 prmorcht 16282 ppiqub 16293 bposlem6 16316 wexmiddiffi 17249