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 (𝜑 ∧ 𝜓)))

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