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 9730 infssfzcldc 10680 infssfzledc 10681 hashfibclem 11298 fzowrddc 11435 bitsinv1 12748 gcdsupex 12753 gcdsupcl 12754 gcdaddm 12780 nnwosdc 12835 lcmval 12860 lcmcllem 12864 lcmledvds 12867 prmdc 12927 pclemdc 13090 infpnlem2 13162 ballotfilemdifcfi 13277 ballotfilemiex 13296 nninfdclemcl 13391 ppiqfi 16203 prmdvdsfi 16204 ppiprm 16220 chtprm 16222 chtdif 16225 efchtqdvds 16226 ppidif 16230 prmorcht 16243 ppiqub 16254 bposlem6 16277 wexmiddiffi 17210