dcan - Intuitionistic Logic Explorer

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

Theorem dcan 923

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 108	. . . . 5 $/\$
2	1	intnanrd 922	. . . 4 $/\$ $/\$
3	2	orim2i 751	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
4		simpr 109	. . . . 5 $\/$ $/\$
5	4	intnand 921	. . . 4 $\/$ $/\$ $/\$
6	5	olcd 724	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$
7	3, 6	jaoi 706	. 2 $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
8		df-dc 825	. . . 4 DECID $\/$
9		df-dc 825	. . . 4 DECID $\/$
10	8, 9	anbi12i 456	. . 3 DECID $/\$ DECID $\/$ $/\$ $\/$
11		andi 808	. . 3 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
12		andir 809	. . . 4 $\/$ $/\$ $/\$ $\/$ $/\$
13	12	orbi1i 753	. . 3 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
14	10, 11, 13	3bitri 205	. 2 DECID $/\$ DECID $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
15		df-dc 825	. 2 DECID $/\$ $/\$ $\/$ $/\$
16	7, 14, 15	3imtr4i 200	1 DECID $/\$ DECID DECID $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103 $\/$ wo 698 DECID wdc 824

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699

This theorem depends on definitions: df-bi 116 df-dc 825

This theorem is referenced by: dcan2 924