Theorem dcand 935

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 837	. . . . 5 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
3		id 19	. . . . . . 7 ⊢ (¬ 𝜓 → ¬ 𝜓)
4	3	intnanrd 934	. . . . . 6 ⊢ (¬ 𝜓 → ¬ (𝜓 ∧ 𝜒))
5	4	orim2i 763	. . . . 5 ⊢ ((𝜓 ∨ ¬ 𝜓) → (𝜓 ∨ ¬ (𝜓 ∧ 𝜒)))
6	2, 5	sylbi 121	. . . 4 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ (𝜓 ∧ 𝜒)))
7	1, 6	syl 14	. . 3 ⊢ (𝜑 → (𝜓 ∨ ¬ (𝜓 ∧ 𝜒)))
8		dcand.2	. . . 4 ⊢ (𝜑 → DECID 𝜒)
9		df-dc 837	. . . . 5 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
10		id 19	. . . . . . 7 ⊢ (¬ 𝜒 → ¬ 𝜒)
11	10	intnand 933	. . . . . 6 ⊢ (¬ 𝜒 → ¬ (𝜓 ∧ 𝜒))
12	11	orim2i 763	. . . . 5 ⊢ ((𝜒 ∨ ¬ 𝜒) → (𝜒 ∨ ¬ (𝜓 ∧ 𝜒)))
13	9, 12	sylbi 121	. . . 4 ⊢ (DECID 𝜒 → (𝜒 ∨ ¬ (𝜓 ∧ 𝜒)))
14	8, 13	syl 14	. . 3 ⊢ (𝜑 → (𝜒 ∨ ¬ (𝜓 ∧ 𝜒)))
15		ordir 819	. . 3 ⊢ (((𝜓 ∧ 𝜒) ∨ ¬ (𝜓 ∧ 𝜒)) ↔ ((𝜓 ∨ ¬ (𝜓 ∧ 𝜒)) ∧ (𝜒 ∨ ¬ (𝜓 ∧ 𝜒))))
16	7, 14, 15	sylanbrc 417	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∨ ¬ (𝜓 ∧ 𝜒)))
17		df-dc 837	. 2 ⊢ (DECID (𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∨ ¬ (𝜓 ∧ 𝜒)))
18	16, 17	sylibr 134	1 ⊢ (𝜑 → DECID (𝜓 ∧ 𝜒))

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

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 615  ax-in2 616  ax-io 711

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

This theorem is referenced by:  dcan  936  dcfi  7090  nn0n0n1ge2b  9459  fzowrddc  11108  bitsinv1  12317  gcdsupex  12322  gcdsupcl  12323  gcdaddm  12349  nnwosdc  12404  lcmval  12429  lcmcllem  12433  lcmledvds  12436  prmdc  12496  pclemdc  12655  infpnlem2  12727  nninfdclemcl  12863