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

Theorem dcbid 782
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 625 . . 3  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
31, 2orbi12d 740 . 2  |-  ( ph  ->  ( ( ps  \/  -.  ps )  <->  ( ch  \/  -.  ch ) ) )
4 df-dc 777 . 2  |-  (DECID  ps  <->  ( ps  \/  -.  ps ) )
5 df-dc 777 . 2  |-  (DECID  ch  <->  ( ch  \/  -.  ch ) )
63, 4, 53bitr4g 221 1  |-  ( ph  ->  (DECID  ps  <-> DECID  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 103    \/ wo 662  DECID wdc 776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115  df-dc 777
This theorem is referenced by:  exmidexmid  3987  exmidel  3990  dcdifsnid  6166  undifdcss  6467  ssfirab  6475  ltdcpi  6627  enqdc  6665  enqdc1  6666  ltdcnq  6701  exfzdc  9378  sumeq1  10393  sumdc  10396  dvdsdc  10411  zdvdsdc  10424  zsupcllemstep  10548  infssuzex  10552  hashdvds  10804  sumdc2  10869
  Copyright terms: Public domain W3C validator