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

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