Theorem dcand 937

Description: A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) (Revised by BJ, 14-Nov-2024.)

Hypotheses

Ref	Expression
dcand.1	⊢ (𝜑 → DECID 𝜓)
dcand.2	⊢ (𝜑 → DECID 𝜒)

Assertion

Ref	Expression
dcand	⊢ (𝜑 → DECID (𝜓 ∧ 𝜒))

Proof of Theorem dcand

Step	Hyp	Ref	Expression
1		dcand.1	. . . 4 ⊢ (𝜑 → DECID 𝜓)
2		df-dc 839	. . . . 5 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
3		id 19	. . . . . . 7 ⊢ (¬ 𝜓 → ¬ 𝜓)
4	3	intnanrd 936	. . . . . 6 ⊢ (¬ 𝜓 → ¬ (𝜓 ∧ 𝜒))
5	4	orim2i 765	. . . . 5 ⊢ ((𝜓 ∨ ¬ 𝜓) → (𝜓 ∨ ¬ (𝜓 ∧ 𝜒)))
6	2, 5	sylbi 121	. . . 4 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ (𝜓 ∧ 𝜒)))
7	1, 6	syl 14	. . 3 ⊢ (𝜑 → (𝜓 ∨ ¬ (𝜓 ∧ 𝜒)))
8		dcand.2	. . . 4 ⊢ (𝜑 → DECID 𝜒)
9		df-dc 839	. . . . 5 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
10		id 19	. . . . . . 7 ⊢ (¬ 𝜒 → ¬ 𝜒)
11	10	intnand 935	. . . . . 6 ⊢ (¬ 𝜒 → ¬ (𝜓 ∧ 𝜒))
12	11	orim2i 765	. . . . 5 ⊢ ((𝜒 ∨ ¬ 𝜒) → (𝜒 ∨ ¬ (𝜓 ∧ 𝜒)))
13	9, 12	sylbi 121	. . . 4 ⊢ (DECID 𝜒 → (𝜒 ∨ ¬ (𝜓 ∧ 𝜒)))
14	8, 13	syl 14	. . 3 ⊢ (𝜑 → (𝜒 ∨ ¬ (𝜓 ∧ 𝜒)))
15		ordir 821	. . 3 ⊢ (((𝜓 ∧ 𝜒) ∨ ¬ (𝜓 ∧ 𝜒)) ↔ ((𝜓 ∨ ¬ (𝜓 ∧ 𝜒)) ∧ (𝜒 ∨ ¬ (𝜓 ∧ 𝜒))))
16	7, 14, 15	sylanbrc 417	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∨ ¬ (𝜓 ∧ 𝜒)))
17		df-dc 839	. 2 ⊢ (DECID (𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∨ ¬ (𝜓 ∧ 𝜒)))
18	16, 17	sylibr 134	1 ⊢ (𝜑 → DECID (𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 712  DECID wdc 838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 713

This theorem depends on definitions:  df-bi 117  df-dc 839

This theorem is referenced by:  dcan  938  dcfi  7116  nn0n0n1ge2b  9494  fzowrddc  11145  bitsinv1  12439  gcdsupex  12444  gcdsupcl  12445  gcdaddm  12471  nnwosdc  12526  lcmval  12551  lcmcllem  12555  lcmledvds  12558  prmdc  12618  pclemdc  12777  infpnlem2  12849  nninfdclemcl  12985