dcan - Intuitionistic Logic Explorer

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

Theorem dcan 875

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 107	. . . . . 6 $/\$
2	1	intnanrd 874	. . . . 5 $/\$ $/\$
3	2	orim2i 710	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
4		simpr 108	. . . . . 6 $\/$ $/\$
5	4	intnand 873	. . . . 5 $\/$ $/\$ $/\$
6	5	olcd 685	. . . 4 $\/$ $/\$ $/\$ $\/$ $/\$
7	3, 6	jaoi 668	. . 3 $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
8		df-dc 776	. . . . 5 DECID $\/$
9		df-dc 776	. . . . 5 DECID $\/$
10	8, 9	anbi12i 447	. . . 4 DECID $/\$ DECID $\/$ $/\$ $\/$
11		andi 764	. . . 4 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
12		andir 765	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$
13	12	orbi1i 712	. . . 4 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
14	10, 11, 13	3bitri 204	. . 3 DECID $/\$ DECID $/\$ $\/$ $/\$ $\/$ $\/$ $/\$
15		df-dc 776	. . 3 DECID $/\$ $/\$ $\/$ $/\$
16	7, 14, 15	3imtr4i 199	. 2 DECID $/\$ DECID DECID $/\$
17	16	ex 113	1 DECID DECID DECID $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 102 $\/$ wo 661 DECID wdc 775

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 576 ax-in2 577 ax-io 662

This theorem depends on definitions: df-bi 115 df-dc 776

This theorem is referenced by: dcbi 877 annimdc 878 pm4.55dc 879 orandc 880 anordc 897 xordidc 1330 nn0n0n1ge2b 8427 gcdmndc 10340 gcdsupex 10349 gcdsupcl 10350 gcdaddm 10375 lcmval 10445 lcmcllem 10449 lcmledvds 10452