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  exmidexmid  4309  exmidel  4318  suppssdc  6460  dcdifsnid  6737  pw2f1odclem  7087  finexdc  7160  elssdc  7162  eqsndc  7163  pw1dc1  7174  undifdcss  7183  prfidceq  7188  tpfidceq  7190  ssfirab  7197  opabfi  7200  infidc  7201  fissfi  7216  fidcenumlemrks  7223  dcfi  7268  2omap  7269  difinfsnlem  7390  difinfsn  7391  ctssdclemn0  7401  ctssdccl  7402  ctssdclemr  7403  ctssdc  7404  iswomni  7456  enwomnilem  7460  nninfdcinf  7462  nninfwlporlem  7464  nninfwlpoimlemdc  7468  nninfinfwlpolem  7469  nninfwlpoim  7470  nninfinfwlpo  7471  netap  7568  ltdcpi  7638  enqdc  7676  enqdc1  7677  ltdcnq  7712  fzodcel  10487  exfzdc  10586  zsupcllemstep  10589  infssuzex  10593  suprzubdc  10596  nninfdcex  10597  zsupssdc  10598  qdcle  10606  hashfibclem  11206  fzowrddc  11339  sumeq1  12040  sumdc  12043  summodclem2  12068  summodc  12069  zsumdc  12070  fsum3  12073  isumz  12075  isumss  12077  fisumss  12078  isumss2  12079  fsum3cvg2  12080  fsumsersdc  12081  fsumsplit  12093  prodeq1f  12238  prodmodclem2a  12262  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodseq  12269  prod1dc  12272  prodssdc  12275  fprodssdc  12276  fprodsplitdc  12282  dvdsdc  12484  zdvdsdc  12498  bitsdc  12633  nnmindc  12730  nnminle  12731  uzwodc  12733  nnwosdc  12735  hashdvds  12918  eulerthlemfi  12925  dvdsfi  12936  phisum  12938  infpnlem2  13058  1arith  13065  4sqexercise1  13096  4sqexercise2  13097  4sqlemsdc  13098  ennnfonelemr  13174  ennnfonelemim  13175  ctinf  13181  ctiunctlemudc  13188  ctiunct  13191  ssomct  13196  ssnnctlemct  13197  nninfdclemcl  13199  nninfdclemp1  13201  psrbagfi  14823  psrbaglecl  14824  psrbagcon  14826  psr1clfi  14843  perfectlem2  15868  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgsval2lem  15883  lgsdir2  15906  lgsne0  15911  2lgs  15977  2lgsoddprm  15986  vtxedgfi  16284  vtxlpfi  16285  eupth2lem3lem4fi  16468  sumdc2  16571  bj-charfundcALT  16579  bj-charfunbi  16581  pw1dceq  16778  nninfsellemdc  16788  iswomninnlem  16834  iswomni0  16836  redcwlpo  16840  redc0  16842  reap0  16843  cndcap  16844  trimul0or  16845  dceqnconst  16846  dcapnconst  16847