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  2935  distrlem4prl  7646  distrlem4pru  7647  exfzdc  10310  lcmmndc  12203  isprm3  12259  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgsval2lem  15167  lgsdir2  15190  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  2lgs  15261  2lgsoddprm  15270  cndcap  15619