Theorem dcand 945

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117  df-dc 847

This theorem is used by:  dcan  946  dcfi  7315  fdcf1  7316  nn0n0n1ge2b  9725  infssfzcldc  10669  infssfzledc  10670  hashfibclem  11282  fzowrddc  11419  bitsinv1  12729  gcdsupex  12734  gcdsupcl  12735  gcdaddm  12761  nnwosdc  12816  lcmval  12841  lcmcllem  12845  lcmledvds  12848  prmdc  12908  pclemdc  13067  infpnlem2  13139  ballotfilemdifcfi  13225  ballotfilemiex  13244  nninfdclemcl  13339  wexmiddiffi  17048