dcan - Intuitionistic Logic Explorer

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

Theorem dcan 919

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

Colors of variables: wff set class

Syntax hints:

wn 3

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

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 821

This theorem is referenced by: dcbi 921 annimdc 922 pm4.55dc 923 orandc 924 anordc 941 xordidc 1378 nn0n0n1ge2b 9154 gcdmndc 11673 gcdsupex 11682 gcdsupcl 11683 gcdaddm 11708 lcmval 11780 lcmcllem 11784 lcmledvds 11787 ctiunctlemudc 11986 nninfsellemdc 13381