Theorem dcand 938

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

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

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 714

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

This theorem is referenced by:  dcan  939  dcfi  7156  nn0n0n1ge2b  9534  fzowrddc  11187  bitsinv1  12481  gcdsupex  12486  gcdsupcl  12487  gcdaddm  12513  nnwosdc  12568  lcmval  12593  lcmcllem  12597  lcmledvds  12600  prmdc  12660  pclemdc  12819  infpnlem2  12891  nninfdclemcl  13027