dcan - Intuitionistic Logic Explorer

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

Theorem dcan 918

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 917	. . . . 5 $/\$ $/\$
3	2	orim2i 750	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
4		simpr 109	. . . . . 6 $\/$ $/\$
5	4	intnand 916	. . . . 5 $\/$ $/\$ $/\$
6	5	olcd 723	. . . 4 $\/$ $/\$ $/\$ $\/$ $/\$
7	3, 6	jaoi 705	. . 3 $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
8		df-dc 820	. . . . 5 DECID $\/$
9		df-dc 820	. . . . 5 DECID $\/$
10	8, 9	anbi12i 455	. . . 4 DECID $/\$ DECID $\/$ $/\$ $\/$
11		andi 807	. . . 4 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
12		andir 808	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$
13	12	orbi1i 752	. . . 4 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
14	10, 11, 13	3bitri 205	. . 3 DECID $/\$ DECID $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
15		df-dc 820	. . 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 697 DECID wdc 819

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 603 ax-in2 604 ax-io 698

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

This theorem is referenced by: dcbi 920 annimdc 921 pm4.55dc 922 orandc 923 anordc 940 xordidc 1377 nn0n0n1ge2b 9130 gcdmndc 11637 gcdsupex 11646 gcdsupcl 11647 gcdaddm 11672 lcmval 11744 lcmcllem 11748 lcmledvds 11751 ctiunctlemudc 11950 nninfsellemdc 13206