Theorem dcor 940

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 839	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2		orc 716	. . . . . 6 ⊢ (𝜑 → (𝜑 ∨ 𝜓))
3	2	orcd 737	. . . . 5 ⊢ (𝜑 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
4		df-dc 839	. . . . 5 ⊢ (DECID (𝜑 ∨ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
5	3, 4	sylibr 134	. . . 4 ⊢ (𝜑 → DECID (𝜑 ∨ 𝜓))
6	5	a1d 22	. . 3 ⊢ (𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
7		df-dc 839	. . . . 5 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
8		olc 715	. . . . . . . . 9 ⊢ (𝜓 → (𝜑 ∨ 𝜓))
9	8	adantl 277	. . . . . . . 8 ⊢ ((¬ 𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜓))
10	9	orcd 737	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ 𝜓) → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
11	10, 4	sylibr 134	. . . . . 6 ⊢ ((¬ 𝜑 ∧ 𝜓) → DECID (𝜑 ∨ 𝜓))
12		ioran 756	. . . . . . . . 9 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
13	12	biimpri 133	. . . . . . . 8 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
14	13	olcd 738	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
15	14, 4	sylibr 134	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → DECID (𝜑 ∨ 𝜓))
16	11, 15	jaodan 801	. . . . 5 ⊢ ((¬ 𝜑 ∧ (𝜓 ∨ ¬ 𝜓)) → DECID (𝜑 ∨ 𝜓))
17	7, 16	sylan2b 287	. . . 4 ⊢ ((¬ 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∨ 𝜓))
18	17	ex 115	. . 3 ⊢ (¬ 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
19	6, 18	jaoi 720	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
20	1, 19	sylbi 121	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → 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:  pm4.55dc  943  orandc  944  pm3.12dc  963  pm3.13dc  964  dn1dc  965  eueq3dc  2957  distrlem4prl  7739  distrlem4pru  7740  exfzdc  10413  lcmmndc  12550  isprm3  12606  perfectlem2  15639  lgsval  15648  lgsfvalg  15649  lgsfcl2  15650  lgsval2lem  15654  lgsdir2  15677  lgsne0  15682  lgsdirnn0  15691  lgsdinn0  15692  2lgs  15748  2lgsoddprm  15757  cndcap  16338