dcan - Intuitionistic Logic Explorer

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

Theorem dcan 928

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 927	. . . 4 $/\$ $/\$
3	2	orim2i 756	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
4		simpr 109	. . . . 5 $\/$ $/\$
5	4	intnand 926	. . . 4 $\/$ $/\$ $/\$
6	5	olcd 729	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$
7	3, 6	jaoi 711	. 2 $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
8		df-dc 830	. . . 4 DECID $\/$
9		df-dc 830	. . . 4 DECID $\/$
10	8, 9	anbi12i 457	. . 3 DECID $/\$ DECID $\/$ $/\$ $\/$
11		andi 813	. . 3 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
12		andir 814	. . . 4 $\/$ $/\$ $/\$ $\/$ $/\$
13	12	orbi1i 758	. . 3 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
14	10, 11, 13	3bitri 205	. 2 DECID $/\$ DECID $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
15		df-dc 830	. 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 703 DECID wdc 829

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 609 ax-in2 610 ax-io 704

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

This theorem is referenced by: dcan2 929