Theorem dcbid 846

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 673	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 801	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 843	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 843	. 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 716  DECID wdc 842

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 619  ax-in2 620  ax-io 717

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

This theorem is referenced by:  dcbiit  847  ifeqeqxdc  3673  exmidexmid  4314  exmidel  4323  suppssdc  6473  dcdifsnid  6750  pw2f1odclem  7100  finexdc  7173  elssdc  7175  eqsndc  7176  pw1dc1  7187  undifdcss  7196  prfidceq  7201  tpfidceq  7203  ssfirab  7210  opabfi  7213  infidc  7214  fissfi  7229  fidcenumlemrks  7236  dcfi  7281  2omap  7282  difinfsnlem  7403  difinfsn  7404  ctssdclemn0  7414  ctssdccl  7415  ctssdclemr  7416  ctssdc  7417  iswomni  7469  enwomnilem  7473  nninfdcinf  7475  nninfwlporlem  7477  nninfwlpoimlemdc  7481  nninfinfwlpolem  7482  nninfwlpoim  7483  nninfinfwlpo  7484  netap  7584  ltdcpi  7654  enqdc  7692  enqdc1  7693  ltdcnq  7728  fzodcel  10509  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  suprzubdc  10620  nninfdcex  10621  zsupssdc  10622  qdcle  10630  hashfibclem  11231  fzowrddc  11364  sumeq1  12065  sumdc  12068  summodclem2  12093  summodc  12094  zsumdc  12095  fsum3  12098  isumz  12100  isumss  12102  fisumss  12103  isumss2  12104  fsum3cvg2  12105  fsumsersdc  12106  fsumsplit  12118  prodeq1f  12263  prodmodclem2a  12287  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodseq  12294  prod1dc  12297  prodssdc  12300  fprodssdc  12301  fprodsplitdc  12307  dvdsdc  12509  zdvdsdc  12523  bitsdc  12658  nnmindc  12755  nnminle  12756  uzwodc  12758  nnwosdc  12760  hashdvds  12943  eulerthlemfi  12950  dvdsfi  12961  phisum  12963  infpnlem2  13083  1arith  13090  4sqexercise1  13121  4sqexercise2  13122  4sqlemsdc  13123  ballotfilemcdc  13167  ballotfilemdifcfz  13171  ballotfilemefi  13181  ennnfonelemr  13258  ennnfonelemim  13259  ctinf  13265  ctiunctlemudc  13272  ctiunct  13275  ssomct  13280  ssnnctlemct  13281  nninfdclemcl  13283  nninfdclemp1  13285  psrbagfi  14949  psrbaglecl  14950  psrbagcon  14952  psr1clfi  14969  perfectlem2  15994  lgsval  16003  lgsfvalg  16004  lgsfcl2  16005  lgsval2lem  16009  lgsdir2  16032  lgsne0  16037  2lgs  16103  2lgsoddprm  16112  vtxedgfi  16410  vtxlpfi  16411  eupth2lem3lem4fi  16594  sumdc2  16697  bj-charfundcALT  16705  bj-charfunbi  16707  pw1dceq  16904  nninfsellemdc  16914  iswomninnlem  16960  iswomni0  16962  redcwlpo  16966  redc0  16968  reap0  16969  cndcap  16970  trimul0or  16971  dceqnconst  16972  dcapnconst  16973