ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dcor GIF version

Theorem dcor 936
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
StepHypRef Expression
1 df-dc 836 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2 orc 713 . . . . . 6 (𝜑 → (𝜑𝜓))
32orcd 734 . . . . 5 (𝜑 → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
4 df-dc 836 . . . . 5 (DECID (𝜑𝜓) ↔ ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
53, 4sylibr 134 . . . 4 (𝜑DECID (𝜑𝜓))
65a1d 22 . . 3 (𝜑 → (DECID 𝜓DECID (𝜑𝜓)))
7 df-dc 836 . . . . 5 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
8 olc 712 . . . . . . . . 9 (𝜓 → (𝜑𝜓))
98adantl 277 . . . . . . . 8 ((¬ 𝜑𝜓) → (𝜑𝜓))
109orcd 734 . . . . . . 7 ((¬ 𝜑𝜓) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
1110, 4sylibr 134 . . . . . 6 ((¬ 𝜑𝜓) → DECID (𝜑𝜓))
12 ioran 753 . . . . . . . . 9 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
1312biimpri 133 . . . . . . . 8 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
1413olcd 735 . . . . . . 7 ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
1514, 4sylibr 134 . . . . . 6 ((¬ 𝜑 ∧ ¬ 𝜓) → DECID (𝜑𝜓))
1611, 15jaodan 798 . . . . 5 ((¬ 𝜑 ∧ (𝜓 ∨ ¬ 𝜓)) → DECID (𝜑𝜓))
177, 16sylan2b 287 . . . 4 ((¬ 𝜑DECID 𝜓) → DECID (𝜑𝜓))
1817ex 115 . . 3 𝜑 → (DECID 𝜓DECID (𝜑𝜓)))
196, 18jaoi 717 . 2 ((𝜑 ∨ ¬ 𝜑) → (DECID 𝜓DECID (𝜑𝜓)))
201, 19sylbi 121 1 (DECID 𝜑 → (DECID 𝜓DECID (𝜑𝜓)))
Colors of variables: wff set class
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  939  orandc  940  pm3.12dc  959  pm3.13dc  960  dn1dc  961  eueq3dc  2923  distrlem4prl  7597  distrlem4pru  7598  exfzdc  10254  lcmmndc  12076  isprm3  12132  lgsval  14758  lgsfvalg  14759  lgsfcl2  14760  lgsval2lem  14764  lgsdir2  14787  lgsne0  14792  lgsdirnn0  14801  lgsdinn0  14802  cndcap  15161
  Copyright terms: Public domain W3C validator