dcan - Intuitionistic Logic Explorer

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

Theorem dcan 933

Description: A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)

**Assertion**
Ref	Expression
dcan	DECID $/\$ DECID DECID $/\$

**Proof of Theorem dcan**
Step	Hyp	Ref	Expression
1		simpl 109	. . . . 5 $/\$
2	1	intnanrd 932	. . . 4 $/\$ $/\$
3	2	orim2i 761	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
4		simpr 110	. . . . 5 $\/$ $/\$
5	4	intnand 931	. . . 4 $\/$ $/\$ $/\$
6	5	olcd 734	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$
7	3, 6	jaoi 716	. 2 $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
8		df-dc 835	. . . 4 DECID $\/$
9		df-dc 835	. . . 4 DECID $\/$
10	8, 9	anbi12i 460	. . 3 DECID $/\$ DECID $\/$ $/\$ $\/$
11		andi 818	. . 3 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
12		andir 819	. . . 4 $\/$ $/\$ $/\$ $\/$ $/\$
13	12	orbi1i 763	. . 3 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
14	10, 11, 13	3bitri 206	. 2 DECID $/\$ DECID $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
15		df-dc 835	. 2 DECID $/\$ $/\$ $\/$ $/\$
16	7, 14, 15	3imtr4i 201	1 DECID $/\$ DECID DECID $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 708 DECID wdc 834

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 614 ax-in2 615 ax-io 709

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

This theorem is referenced by: dcan2 934