Theorem dcbid 840

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 669	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 795	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 837	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 837	. 2 |- (DECID ch <-> ( ch \/ -. ch ) )
6	3, 4, 5	3bitr4g 223	1 |- ( ph -> (DECID ps <-> DECID ch ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105   \/ wo 710  DECID wdc 836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711

This theorem depends on definitions:  df-bi 117  df-dc 837

This theorem is referenced by:  dcbiit  841  exmidexmid  4241  exmidel  4250  dcdifsnid  6592  pw2f1odclem  6933  finexdc  7001  pw1dc1  7013  undifdcss  7022  prfidceq  7027  tpfidceq  7029  ssfirab  7035  opabfi  7037  infidc  7038  fidcenumlemrks  7057  dcfi  7085  difinfsnlem  7203  difinfsn  7204  ctssdclemn0  7214  ctssdccl  7215  ctssdclemr  7216  ctssdc  7217  iswomni  7269  enwomnilem  7273  nninfdcinf  7275  nninfwlporlem  7277  nninfwlpoimlemdc  7281  nninfinfwlpolem  7282  nninfwlpoim  7283  nninfinfwlpo  7284  netap  7368  ltdcpi  7438  enqdc  7476  enqdc1  7477  ltdcnq  7512  fzodcel  10277  exfzdc  10371  zsupcllemstep  10374  infssuzex  10378  suprzubdc  10381  nninfdcex  10382  zsupssdc  10383  qdcle  10391  fzowrddc  11103  sumeq1  11699  sumdc  11702  summodclem2  11726  summodc  11727  zsumdc  11728  fsum3  11731  isumz  11733  isumss  11735  fisumss  11736  isumss2  11737  fsum3cvg2  11738  fsumsersdc  11739  fsumsplit  11751  prodeq1f  11896  prodmodclem2a  11920  prodmodclem2  11921  prodmodc  11922  zproddc  11923  fprodseq  11927  prod1dc  11930  prodssdc  11933  fprodssdc  11934  fprodsplitdc  11940  dvdsdc  12142  zdvdsdc  12156  bitsdc  12291  nnmindc  12388  nnminle  12389  uzwodc  12391  nnwosdc  12393  hashdvds  12576  eulerthlemfi  12583  dvdsfi  12594  phisum  12596  infpnlem2  12716  1arith  12723  4sqexercise1  12754  4sqexercise2  12755  4sqlemsdc  12756  ennnfonelemr  12827  ennnfonelemim  12828  ctinf  12834  ctiunctlemudc  12841  ctiunct  12844  ssomct  12849  ssnnctlemct  12850  nninfdclemcl  12852  nninfdclemp1  12854  psrbagfi  14468  psr1clfi  14483  perfectlem2  15505  lgsval  15514  lgsfvalg  15515  lgsfcl2  15516  lgsval2lem  15520  lgsdir2  15543  lgsne0  15548  2lgs  15614  2lgsoddprm  15623  sumdc2  15772  bj-charfundcALT  15782  bj-charfunbi  15784  2omap  15969  nninfsellemdc  15984  iswomninnlem  16025  iswomni0  16027  redcwlpo  16031  redc0  16033  reap0  16034  cndcap  16035  dceqnconst  16036  dcapnconst  16037