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

Theorem dcor 935
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 835 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2 orc 712 . . . . . 6 (𝜑 → (𝜑𝜓))
32orcd 733 . . . . 5 (𝜑 → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
4 df-dc 835 . . . . 5 (DECID (𝜑𝜓) ↔ ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
53, 4sylibr 134 . . . 4 (𝜑DECID (𝜑𝜓))
65a1d 22 . . 3 (𝜑 → (DECID 𝜓DECID (𝜑𝜓)))
7 df-dc 835 . . . . 5 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
8 olc 711 . . . . . . . . 9 (𝜓 → (𝜑𝜓))
98adantl 277 . . . . . . . 8 ((¬ 𝜑𝜓) → (𝜑𝜓))
109orcd 733 . . . . . . 7 ((¬ 𝜑𝜓) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
1110, 4sylibr 134 . . . . . 6 ((¬ 𝜑𝜓) → DECID (𝜑𝜓))
12 ioran 752 . . . . . . . . 9 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
1312biimpri 133 . . . . . . . 8 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
1413olcd 734 . . . . . . 7 ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
1514, 4sylibr 134 . . . . . 6 ((¬ 𝜑 ∧ ¬ 𝜓) → DECID (𝜑𝜓))
1611, 15jaodan 797 . . . . 5 ((¬ 𝜑 ∧ (𝜓 ∨ ¬ 𝜓)) → DECID (𝜑𝜓))
177, 16sylan2b 287 . . . 4 ((¬ 𝜑DECID 𝜓) → DECID (𝜑𝜓))
1817ex 115 . . 3 𝜑 → (DECID 𝜓DECID (𝜑𝜓)))
196, 18jaoi 716 . 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 708  DECID wdc 834
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 614  ax-in2 615  ax-io 709
This theorem depends on definitions:  df-bi 117  df-dc 835
This theorem is referenced by:  pm4.55dc  938  orandc  939  pm3.12dc  958  pm3.13dc  959  dn1dc  960  eueq3dc  2911  distrlem4prl  7582  distrlem4pru  7583  exfzdc  10239  lcmmndc  12061  isprm3  12117  lgsval  14375  lgsfvalg  14376  lgsfcl2  14377  lgsval2lem  14381  lgsdir2  14404  lgsne0  14409  lgsdirnn0  14418  lgsdinn0  14419
  Copyright terms: Public domain W3C validator