dcand - Intuitionistic Logic Explorer

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

Theorem dcand 940

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 842	. . . . 5 DECID $\/$
3		id 19	. . . . . . 7
4	3	intnanrd 939	. . . . . 6 $/\$
5	4	orim2i 768	. . . . 5 $\/$ $\/$ $/\$
6	2, 5	sylbi 121	. . . 4 DECID $\/$ $/\$
7	1, 6	syl 14	. . 3 $\/$ $/\$
8		dcand.2	. . . 4 DECID
9		df-dc 842	. . . . 5 DECID $\/$
10		id 19	. . . . . . 7
11	10	intnand 938	. . . . . 6 $/\$
12	11	orim2i 768	. . . . 5 $\/$ $\/$ $/\$
13	9, 12	sylbi 121	. . . 4 DECID $\/$ $/\$
14	8, 13	syl 14	. . 3 $\/$ $/\$
15		ordir 824	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
16	7, 14, 15	sylanbrc 417	. 2 $/\$ $\/$ $/\$
17		df-dc 842	. 2 DECID $/\$ $/\$ $\/$ $/\$
18	16, 17	sylibr 134	1 DECID $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 715 DECID wdc 841

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 619 ax-in2 620 ax-io 716

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

This theorem is referenced by: dcan 941 dcfi 7180 nn0n0n1ge2b 9559 fzowrddc 11232 bitsinv1 12541 gcdsupex 12546 gcdsupcl 12547 gcdaddm 12573 nnwosdc 12628 lcmval 12653 lcmcllem 12657 lcmledvds 12660 prmdc 12720 pclemdc 12879 infpnlem2 12951 nninfdclemcl 13087