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 7315 fdcf1 7316 nn0n0n1ge2b 9729 infssfzcldc 10679 infssfzledc 10680 hashfibclem 11296 fzowrddc 11433 bitsinv1 12745 gcdsupex 12750 gcdsupcl 12751 gcdaddm 12777 nnwosdc 12832 lcmval 12857 lcmcllem 12861 lcmledvds 12864 prmdc 12924 pclemdc 13087 infpnlem2 13159 ballotfilemdifcfi 13274 ballotfilemiex 13293 nninfdclemcl 13388 ppiqfi 16158 prmdvdsfi 16159 ppiprm 16170 ppidif 16175 ppiqub 16194 wexmiddiffi 17142