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 7179 nn0n0n1ge2b 9558 fzowrddc 11227 bitsinv1 12522 gcdsupex 12527 gcdsupcl 12528 gcdaddm 12554 nnwosdc 12609 lcmval 12634 lcmcllem 12638 lcmledvds 12641 prmdc 12701 pclemdc 12860 infpnlem2 12932 nninfdclemcl 13068