Theorem dcbid 850

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 677	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 805	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 847	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 847	. 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 720  DECID wdc 846

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 623  ax-in2 624  ax-io 721

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

This theorem is referenced by:  dcbiit  851  ifeqeqxdc  3684  exmidexmid  4328  exmidel  4337  suppssdc  6490  dcdifsnid  6767  pw2f1odclem  7124  finexdc  7197  elssdc  7199  eqsndc  7200  pw1dc1  7211  undifdcss  7220  prfidceq  7225  tpfidceq  7227  ssfirab  7234  opabfi  7237  infidc  7238  fissfi  7253  fidcenumlemrks  7260  dcfi  7305  2omap  7308  difinfsnlem  7429  difinfsn  7430  ctssdclemn0  7440  ctssdccl  7441  ctssdclemr  7442  ctssdc  7443  iswomni  7495  enwomnilem  7499  nninfdcinf  7501  nninfwlporlem  7503  nninfwlpoimlemdc  7507  nninfinfwlpolem  7508  nninfwlpoim  7509  nninfinfwlpo  7510  netap  7610  ltdcpi  7680  enqdc  7718  enqdc1  7719  ltdcnq  7754  fzodcel  10538  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  suprzubdc  10649  nninfdcex  10650  zsupssdc  10651  qdcle  10659  hashfibclem  11260  fzowrddc  11397  sumeq1  12099  sumdc  12102  summodclem2  12127  summodc  12128  zsumdc  12129  fsum3  12132  isumz  12134  isumss  12136  fisumss  12137  isumss2  12138  fsum3cvg2  12139  fsumsersdc  12140  fsumsplit  12152  prodeq1f  12297  prodmodclem2a  12321  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodseq  12328  prod1dc  12331  prodssdc  12334  fprodssdc  12335  fprodsplitdc  12341  dvdsdc  12543  zdvdsdc  12557  bitsdc  12692  nnmindc  12789  nnminle  12790  uzwodc  12792  nnwosdc  12794  hashdvds  12977  eulerthlemfi  12984  dvdsfi  12995  phisum  12997  infpnlem2  13117  1arith  13124  4sqexercise1  13155  4sqexercise2  13156  4sqlemsdc  13157  ballotfilemcdc  13201  ballotfilemdifcfz  13205  ballotfilemefi  13215  ennnfonelemr  13292  ennnfonelemim  13293  ctinf  13299  ctiunctlemudc  13306  ctiunct  13309  ssomct  13314  ssnnctlemct  13315  nninfdclemcl  13317  nninfdclemp1  13319  psrbagfi  14982  psrbaglecl  14983  psrbagcon  14985  psr1clfi  15002  perfectlem2  16028  lgsval  16037  lgsfvalg  16038  lgsfcl2  16039  lgsval2lem  16043  lgsdir2  16066  lgsne0  16071  2lgs  16137  2lgsoddprm  16146  vtxedgfi  16444  vtxlpfi  16445  eupth2lem3lem4fi  16628  sumdc2  16741  bj-charfundcALT  16749  bj-charfunbi  16751  pw1dceq  16948  nninfsellemdc  16958  iswomninnlem  17004  iswomni0  17006  redcwlpo  17010  redc0  17012  reap0  17013  cndcap  17014  dceqnconst  17015  dcapnconst  17016