Theorem dcbid 824

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

Step	Hyp	Ref	Expression
1		dcbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	notbid 657	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 783	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 821	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 821	. 2 |- (DECID ch <-> ( ch \/ -. ch ) )
6	3, 4, 5	3bitr4g 222	1 |- ( ph -> (DECID ps <-> DECID ch ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   \/ 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:  dcbiit  825  exmidexmid  4157  exmidel  4166  dcdifsnid  6451  finexdc  6847  pw1dc1  6858  undifdcss  6867  ssfirab  6878  fidcenumlemrks  6897  dcfi  6925  difinfsnlem  7043  difinfsn  7044  ctssdclemn0  7054  ctssdccl  7055  ctssdclemr  7056  ctssdc  7057  iswomni  7108  enwomnilem  7112  ltdcpi  7243  enqdc  7281  enqdc1  7282  ltdcnq  7317  fzodcel  10051  exfzdc  10139  sumeq1  11252  sumdc  11255  summodclem2  11279  summodc  11280  zsumdc  11281  fsum3  11284  isumz  11286  isumss  11288  fisumss  11289  isumss2  11290  fsum3cvg2  11291  fsumsersdc  11292  fsumsplit  11304  prodeq1f  11449  prodmodclem2a  11473  prodmodclem2  11474  prodmodc  11475  zproddc  11476  fprodseq  11480  prod1dc  11483  prodssdc  11486  fprodssdc  11487  fprodsplitdc  11493  dvdsdc  11694  zdvdsdc  11707  zsupcllemstep  11831  infssuzex  11835  nninfdcex  11838  hashdvds  12095  eulerthlemfi  12102  phisum  12114  ennnfonelemr  12152  ennnfonelemim  12153  ctinf  12159  ctiunctlemudc  12166  ctiunct  12169  ssomct  12174  ssnnctlemct  12175  nnmindc  12177  nnminle  12178  nninfdclemcl  12179  nninfdclemp1  12181  sumdc2  13373  bj-charfundcALT  13384  bj-charfunbi  13386  nninfsellemdc  13582  iswomninnlem  13620  iswomni0  13622  redcwlpo  13626  redc0  13628  reap0  13629  dceqnconst  13630  dcapnconst  13631