dcand - Intuitionistic Logic Explorer

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

Theorem dcand 938

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

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 713 DECID wdc 839

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 617 ax-in2 618 ax-io 714

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

This theorem is referenced by: dcan 939 dcfi 7159 nn0n0n1ge2b 9537 fzowrddc 11194 bitsinv1 12488 gcdsupex 12493 gcdsupcl 12494 gcdaddm 12520 nnwosdc 12575 lcmval 12600 lcmcllem 12604 lcmledvds 12607 prmdc 12667 pclemdc 12826 infpnlem2 12898 nninfdclemcl 13034