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

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 720 DECID wdc 846

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 623 ax-in2 624 ax-io 721

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

This theorem is referenced by: dcan 946 dcfi 7305 fdcf1 7306 nn0n0n1ge2b 9704 infssfzcldc 10647 infssfzledc 10648 hashfibclem 11260 fzowrddc 11397 bitsinv1 12707 gcdsupex 12712 gcdsupcl 12713 gcdaddm 12739 nnwosdc 12794 lcmval 12819 lcmcllem 12823 lcmledvds 12826 prmdc 12886 pclemdc 13045 infpnlem2 13117 ballotfilemdifcfi 13203 ballotfilemiex 13222 nninfdclemcl 13317