Theorem dcor 829

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 731	. 2 ⊢ (DECID φ ↔ (φ ∨ ¬ φ))
2		orc 620	. . . . . 6 ⊢ (φ → (φ ∨ ψ))
3	2	orcd 639	. . . . 5 ⊢ (φ → ((φ ∨ ψ) ∨ ¬ (φ ∨ ψ)))
4		df-dc 731	. . . . 5 ⊢ (DECID (φ ∨ ψ) ↔ ((φ ∨ ψ) ∨ ¬ (φ ∨ ψ)))
5	3, 4	sylibr 137	. . . 4 ⊢ (φ → DECID (φ ∨ ψ))
6	5	a1d 22	. . 3 ⊢ (φ → (DECID ψ → DECID (φ ∨ ψ)))
7		df-dc 731	. . . . 5 ⊢ (DECID ψ ↔ (ψ ∨ ¬ ψ))
8		olc 619	. . . . . . . . 9 ⊢ (ψ → (φ ∨ ψ))
9	8	adantl 262	. . . . . . . 8 ⊢ ((¬ φ ∧ ψ) → (φ ∨ ψ))
10	9	orcd 639	. . . . . . 7 ⊢ ((¬ φ ∧ ψ) → ((φ ∨ ψ) ∨ ¬ (φ ∨ ψ)))
11	10, 4	sylibr 137	. . . . . 6 ⊢ ((¬ φ ∧ ψ) → DECID (φ ∨ ψ))
12		ioran 656	. . . . . . . . 9 ⊢ (¬ (φ ∨ ψ) ↔ (¬ φ ∧ ¬ ψ))
13	12	biimpri 124	. . . . . . . 8 ⊢ ((¬ φ ∧ ¬ ψ) → ¬ (φ ∨ ψ))
14	13	olcd 640	. . . . . . 7 ⊢ ((¬ φ ∧ ¬ ψ) → ((φ ∨ ψ) ∨ ¬ (φ ∨ ψ)))
15	14, 4	sylibr 137	. . . . . 6 ⊢ ((¬ φ ∧ ¬ ψ) → DECID (φ ∨ ψ))
16	11, 15	jaodan 697	. . . . 5 ⊢ ((¬ φ ∧ (ψ ∨ ¬ ψ)) → DECID (φ ∨ ψ))
17	7, 16	sylan2b 271	. . . 4 ⊢ ((¬ φ ∧ DECID ψ) → DECID (φ ∨ ψ))
18	17	ex 108	. . 3 ⊢ (¬ φ → (DECID ψ → DECID (φ ∨ ψ)))
19	6, 18	jaoi 623	. 2 ⊢ ((φ ∨ ¬ φ) → (DECID ψ → DECID (φ ∨ ψ)))
20	1, 19	sylbi 114	1 ⊢ (DECID φ → (DECID ψ → DECID (φ ∨ ψ)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 616  DECID wdc 730

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617

This theorem depends on definitions:  df-bi 110  df-dc 731

This theorem is referenced by:  pm4.55dc  832  pm3.12dc  851  pm3.13dc  852  dn1dc  853  eueq3dc  2688  distrlem4prl  6417  distrlem4pru  6418