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

Theorem dcbid 808
Description: Equivalence property for decidability. Deduction form. (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 641 . . 3  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
31, 2orbi12d 767 . 2  |-  ( ph  ->  ( ( ps  \/  -.  ps )  <->  ( ch  \/  -.  ch ) ) )
4 df-dc 805 . 2  |-  (DECID  ps  <->  ( ps  \/  -.  ps ) )
5 df-dc 805 . 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 682  DECID wdc 804
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 588  ax-in2 589  ax-io 683
This theorem depends on definitions:  df-bi 116  df-dc 805
This theorem is referenced by:  dcbiit  809  exmidexmid  4090  exmidel  4098  dcdifsnid  6368  finexdc  6764  undifdcss  6779  ssfirab  6790  fidcenumlemrks  6809  difinfsnlem  6952  difinfsn  6953  ctssdclemn0  6963  ctssdccl  6964  ctssdclemr  6965  ctssdc  6966  ltdcpi  7099  enqdc  7137  enqdc1  7138  ltdcnq  7173  fzodcel  9884  exfzdc  9972  sumeq1  11079  sumdc  11082  summodclem2  11106  summodc  11107  zsumdc  11108  fsum3  11111  isumz  11113  isumss  11115  fisumss  11116  isumss2  11117  fsum3cvg2  11118  fsumsersdc  11119  fsumsplit  11131  dvdsdc  11413  zdvdsdc  11426  zsupcllemstep  11550  infssuzex  11554  hashdvds  11808  ennnfonelemr  11847  ennnfonelemim  11848  ctinf  11854  ctiunctlemudc  11861  ctiunct  11864  sumdc2  12902  nninfsellemdc  13102
  Copyright terms: Public domain W3C validator