Theorem dcor 842

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 742	. 2 ⊢ (DECID φ ↔ (φ ∨ ¬ φ))
2		orc 632	. . . . . 6 ⊢ (φ → (φ ∨ ψ))
3	2	orcd 651	. . . . 5 ⊢ (φ → ((φ ∨ ψ) ∨ ¬ (φ ∨ ψ)))
4		df-dc 742	. . . . 5 ⊢ (DECID (φ ∨ ψ) ↔ ((φ ∨ ψ) ∨ ¬ (φ ∨ ψ)))
5	3, 4	sylibr 137	. . . 4 ⊢ (φ → DECID (φ ∨ ψ))
6	5	a1d 22	. . 3 ⊢ (φ → (DECID ψ → DECID (φ ∨ ψ)))
7		df-dc 742	. . . . 5 ⊢ (DECID ψ ↔ (ψ ∨ ¬ ψ))
8		olc 631	. . . . . . . . 9 ⊢ (ψ → (φ ∨ ψ))
9	8	adantl 262	. . . . . . . 8 ⊢ ((¬ φ ∧ ψ) → (φ ∨ ψ))
10	9	orcd 651	. . . . . . 7 ⊢ ((¬ φ ∧ ψ) → ((φ ∨ ψ) ∨ ¬ (φ ∨ ψ)))
11	10, 4	sylibr 137	. . . . . 6 ⊢ ((¬ φ ∧ ψ) → DECID (φ ∨ ψ))
12		ioran 668	. . . . . . . . 9 ⊢ (¬ (φ ∨ ψ) ↔ (¬ φ ∧ ¬ ψ))
13	12	biimpri 124	. . . . . . . 8 ⊢ ((¬ φ ∧ ¬ ψ) → ¬ (φ ∨ ψ))
14	13	olcd 652	. . . . . . 7 ⊢ ((¬ φ ∧ ¬ ψ) → ((φ ∨ ψ) ∨ ¬ (φ ∨ ψ)))
15	14, 4	sylibr 137	. . . . . 6 ⊢ ((¬ φ ∧ ¬ ψ) → DECID (φ ∨ ψ))
16	11, 15	jaodan 709	. . . . 5 ⊢ ((¬ φ ∧ (ψ ∨ ¬ ψ)) → DECID (φ ∨ ψ))
17	7, 16	sylan2b 271	. . . 4 ⊢ ((¬ φ ∧ DECID ψ) → DECID (φ ∨ ψ))
18	17	ex 108	. . 3 ⊢ (¬ φ → (DECID ψ → DECID (φ ∨ ψ)))
19	6, 18	jaoi 635	. 2 ⊢ ((φ ∨ ¬ φ) → (DECID ψ → DECID (φ ∨ ψ)))
20	1, 19	sylbi 114	1 ⊢ (DECID φ → (DECID ψ → DECID (φ ∨ ψ)))

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

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 544  ax-in2 545  ax-io 629

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

This theorem is referenced by:  pm4.55dc  845  pm3.12dc  864  pm3.13dc  865  dn1dc  866  eueq3dc  2709  distrlem4prl  6560  distrlem4pru  6561