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 9725 infssfzcldc 10669 infssfzledc 10670 hashfibclem 11282 fzowrddc 11419 bitsinv1 12729 gcdsupex 12734 gcdsupcl 12735 gcdaddm 12761 nnwosdc 12816 lcmval 12841 lcmcllem 12845 lcmledvds 12848 prmdc 12908 pclemdc 13067 infpnlem2 13139 ballotfilemdifcfi 13225 ballotfilemiex 13244 nninfdclemcl 13339 wexmiddiffi 17044