Theorem dcor 925

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 825	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2		orc 702	. . . . . 6 ⊢ (𝜑 → (𝜑 ∨ 𝜓))
3	2	orcd 723	. . . . 5 ⊢ (𝜑 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
4		df-dc 825	. . . . 5 ⊢ (DECID (𝜑 ∨ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
5	3, 4	sylibr 133	. . . 4 ⊢ (𝜑 → DECID (𝜑 ∨ 𝜓))
6	5	a1d 22	. . 3 ⊢ (𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
7		df-dc 825	. . . . 5 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
8		olc 701	. . . . . . . . 9 ⊢ (𝜓 → (𝜑 ∨ 𝜓))
9	8	adantl 275	. . . . . . . 8 ⊢ ((¬ 𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜓))
10	9	orcd 723	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ 𝜓) → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
11	10, 4	sylibr 133	. . . . . 6 ⊢ ((¬ 𝜑 ∧ 𝜓) → DECID (𝜑 ∨ 𝜓))
12		ioran 742	. . . . . . . . 9 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
13	12	biimpri 132	. . . . . . . 8 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
14	13	olcd 724	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
15	14, 4	sylibr 133	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → DECID (𝜑 ∨ 𝜓))
16	11, 15	jaodan 787	. . . . 5 ⊢ ((¬ 𝜑 ∧ (𝜓 ∨ ¬ 𝜓)) → DECID (𝜑 ∨ 𝜓))
17	7, 16	sylan2b 285	. . . 4 ⊢ ((¬ 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∨ 𝜓))
18	17	ex 114	. . 3 ⊢ (¬ 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
19	6, 18	jaoi 706	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
20	1, 19	sylbi 120	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 698  DECID wdc 824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116  df-dc 825

This theorem is referenced by:  pm4.55dc  928  orandc  929  pm3.12dc  948  pm3.13dc  949  dn1dc  950  eueq3dc  2900  distrlem4prl  7525  distrlem4pru  7526  exfzdc  10175  lcmmndc  11994  isprm3  12050  lgsval  13545  lgsfvalg  13546  lgsfcl2  13547  lgsval2lem  13551  lgsdir2  13574  lgsne0  13579  lgsdirnn0  13588  lgsdinn0  13589