Theorem dcor 937

Description: A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)

Assertion

Ref	Expression
dcor	⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))

Proof of Theorem dcor

Step	Hyp	Ref	Expression
1		df-dc 836	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2		orc 713	. . . . . 6 ⊢ (𝜑 → (𝜑 ∨ 𝜓))
3	2	orcd 734	. . . . 5 ⊢ (𝜑 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
4		df-dc 836	. . . . 5 ⊢ (DECID (𝜑 ∨ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
5	3, 4	sylibr 134	. . . 4 ⊢ (𝜑 → DECID (𝜑 ∨ 𝜓))
6	5	a1d 22	. . 3 ⊢ (𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
7		df-dc 836	. . . . 5 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
8		olc 712	. . . . . . . . 9 ⊢ (𝜓 → (𝜑 ∨ 𝜓))
9	8	adantl 277	. . . . . . . 8 ⊢ ((¬ 𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜓))
10	9	orcd 734	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ 𝜓) → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
11	10, 4	sylibr 134	. . . . . 6 ⊢ ((¬ 𝜑 ∧ 𝜓) → DECID (𝜑 ∨ 𝜓))
12		ioran 753	. . . . . . . . 9 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
13	12	biimpri 133	. . . . . . . 8 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
14	13	olcd 735	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
15	14, 4	sylibr 134	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → DECID (𝜑 ∨ 𝜓))
16	11, 15	jaodan 798	. . . . 5 ⊢ ((¬ 𝜑 ∧ (𝜓 ∨ ¬ 𝜓)) → DECID (𝜑 ∨ 𝜓))
17	7, 16	sylan2b 287	. . . 4 ⊢ ((¬ 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∨ 𝜓))
18	17	ex 115	. . 3 ⊢ (¬ 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
19	6, 18	jaoi 717	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
20	1, 19	sylbi 121	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))

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

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 710

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

This theorem is referenced by:  pm4.55dc  940  orandc  941  pm3.12dc  960  pm3.13dc  961  dn1dc  962  eueq3dc  2938  distrlem4prl  7668  distrlem4pru  7669  exfzdc  10333  lcmmndc  12255  isprm3  12311  perfectlem2  15320  lgsval  15329  lgsfvalg  15330  lgsfcl2  15331  lgsval2lem  15335  lgsdir2  15358  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  2lgs  15429  2lgsoddprm  15438  cndcap  15790