Theorem dcor 944

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 843	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2		orc 720	. . . . . 6 ⊢ (𝜑 → (𝜑 ∨ 𝜓))
3	2	orcd 741	. . . . 5 ⊢ (𝜑 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
4		df-dc 843	. . . . 5 ⊢ (DECID (𝜑 ∨ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
5	3, 4	sylibr 134	. . . 4 ⊢ (𝜑 → DECID (𝜑 ∨ 𝜓))
6	5	a1d 22	. . 3 ⊢ (𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
7		df-dc 843	. . . . 5 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
8		olc 719	. . . . . . . . 9 ⊢ (𝜓 → (𝜑 ∨ 𝜓))
9	8	adantl 277	. . . . . . . 8 ⊢ ((¬ 𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜓))
10	9	orcd 741	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ 𝜓) → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
11	10, 4	sylibr 134	. . . . . 6 ⊢ ((¬ 𝜑 ∧ 𝜓) → DECID (𝜑 ∨ 𝜓))
12		ioran 760	. . . . . . . . 9 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
13	12	biimpri 133	. . . . . . . 8 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
14	13	olcd 742	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
15	14, 4	sylibr 134	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → DECID (𝜑 ∨ 𝜓))
16	11, 15	jaodan 805	. . . . 5 ⊢ ((¬ 𝜑 ∧ (𝜓 ∨ ¬ 𝜓)) → DECID (𝜑 ∨ 𝜓))
17	7, 16	sylan2b 287	. . . 4 ⊢ ((¬ 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∨ 𝜓))
18	17	ex 115	. . 3 ⊢ (¬ 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
19	6, 18	jaoi 724	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
20	1, 19	sylbi 121	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))

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

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 619  ax-in2 620  ax-io 717

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

This theorem is referenced by:  pm4.55dc  947  orandc  948  pm3.12dc  967  pm3.13dc  968  dn1dc  969  eueq3dc  2993  distrlem4prl  7904  distrlem4pru  7905  exfzdc  10593  lcmmndc  12767  isprm3  12823  perfectlem2  15917  lgsval  15926  lgsfvalg  15927  lgsfcl2  15928  lgsval2lem  15932  lgsdir2  15955  lgsne0  15960  lgsdirnn0  15969  lgsdinn0  15970  2lgs  16026  2lgsoddprm  16035  eupth2lem3lem4fi  16517  eupth2lem3lem7fi  16518  cndcap  16893