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

Theorem dcor 920
 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 821 . 2 DECID
2 orc 702 . . . . . 6
32orcd 723 . . . . 5
4 df-dc 821 . . . . 5 DECID
53, 4sylibr 133 . . . 4 DECID
65a1d 22 . . 3 DECID DECID
7 df-dc 821 . . . . 5 DECID
8 olc 701 . . . . . . . . 9
98adantl 275 . . . . . . . 8
109orcd 723 . . . . . . 7
1110, 4sylibr 133 . . . . . 6 DECID
12 ioran 742 . . . . . . . . 9
1312biimpri 132 . . . . . . . 8
1413olcd 724 . . . . . . 7
1514, 4sylibr 133 . . . . . 6 DECID
1611, 15jaodan 787 . . . . 5 DECID
177, 16sylan2b 285 . . . 4 DECID DECID
1817ex 114 . . 3 DECID DECID
196, 18jaoi 706 . 2 DECID DECID
201, 19sylbi 120 1 DECID DECID DECID
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wo 698  DECID wdc 820 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 821 This theorem is referenced by:  pm4.55dc  923  orandc  924  pm3.12dc  943  pm3.13dc  944  dn1dc  945  eueq3dc  2886  distrlem4prl  7487  distrlem4pru  7488  exfzdc  10121  lcmmndc  11919  isprm3  11975
 Copyright terms: Public domain W3C validator