dcan - Intuitionistic Logic Explorer

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

Theorem dcan 842

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 102	. . . . . 6 $/\$
2	1	intnanrd 841	. . . . 5 $/\$ $/\$
3	2	orim2i 678	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
4		simpr 103	. . . . . 6 $\/$ $/\$
5	4	intnand 840	. . . . 5 $\/$ $/\$ $/\$
6	5	olcd 653	. . . 4 $\/$ $/\$ $/\$ $\/$ $/\$
7	3, 6	jaoi 636	. . 3 $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
8		df-dc 743	. . . . 5 DECID $\/$
9		df-dc 743	. . . . 5 DECID $\/$
10	8, 9	anbi12i 433	. . . 4 DECID $/\$ DECID $\/$ $/\$ $\/$
11		andi 731	. . . 4 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
12		andir 732	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$
13	12	orbi1i 680	. . . 4 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
14	10, 11, 13	3bitri 195	. . 3 DECID $/\$ DECID $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
15		df-dc 743	. . 3 DECID $/\$ $/\$ $\/$ $/\$
16	7, 14, 15	3imtr4i 190	. 2 DECID $/\$ DECID DECID $/\$
17	16	ex 108	1 DECID DECID DECID $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 97 $\/$ wo 629 DECID wdc 742

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630

This theorem depends on definitions: df-bi 110 df-dc 743

This theorem is referenced by: dcbi 844 annimdc 845 pm4.55dc 846 anordc 863 xordidc 1290 nn0n0n1ge2b 8320