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

Theorem dcbid 787
Description: The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
Hypothesis
Ref Expression
dcbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
dcbid  |-  ( ph  ->  (DECID  ps  <-> DECID  ch ) )

Proof of Theorem dcbid
StepHypRef Expression
1 dcbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21notbid 628 . . 3  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
31, 2orbi12d 743 . 2  |-  ( ph  ->  ( ( ps  \/  -.  ps )  <->  ( ch  \/  -.  ch ) ) )
4 df-dc 782 . 2  |-  (DECID  ps  <->  ( ps  \/  -.  ps ) )
5 df-dc 782 . 2  |-  (DECID  ch  <->  ( ch  \/  -.  ch ) )
63, 4, 53bitr4g 222 1  |-  ( ph  ->  (DECID  ps  <-> DECID  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104    \/ wo 665  DECID wdc 781
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666
This theorem depends on definitions:  df-bi 116  df-dc 782
This theorem is referenced by:  exmidexmid  4039  exmidel  4044  dcdifsnid  6279  finexdc  6674  undifdcss  6689  ssfirab  6699  fidcenumlemrks  6718  ltdcpi  6945  enqdc  6983  enqdc1  6984  ltdcnq  7019  fzodcel  9626  exfzdc  9714  sumeq1  10807  sumdc  10810  isummolem2  10835  isummo  10836  zisum  10837  fisum  10841  isumz  10844  isumss  10846  fisumss  10847  isumss2  10848  fisumcvg2  10849  fsum3cvg2  10850  fisumsers  10851  fsumsplit  10864  dvdsdc  11145  zdvdsdc  11158  zsupcllemstep  11282  infssuzex  11286  hashdvds  11538  sumdc2  12003  nninfsellemdc  12205
  Copyright terms: Public domain W3C validator