Theorem dcbid 845

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 800	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 842	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 842	. 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 715  DECID wdc 841

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 716

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

This theorem is referenced by:  dcbiit  846  exmidexmid  4286  exmidel  4295  dcdifsnid  6672  pw2f1odclem  7020  finexdc  7092  elssdc  7094  eqsndc  7095  pw1dc1  7106  undifdcss  7115  prfidceq  7120  tpfidceq  7122  ssfirab  7129  opabfi  7132  infidc  7133  fidcenumlemrks  7152  dcfi  7180  difinfsnlem  7298  difinfsn  7299  ctssdclemn0  7309  ctssdccl  7310  ctssdclemr  7311  ctssdc  7312  iswomni  7364  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemdc  7376  nninfinfwlpolem  7377  nninfwlpoim  7378  nninfinfwlpo  7379  netap  7473  ltdcpi  7543  enqdc  7581  enqdc1  7582  ltdcnq  7617  fzodcel  10388  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  nninfdcex  10498  zsupssdc  10499  qdcle  10507  fzowrddc  11232  sumeq1  11933  sumdc  11936  summodclem2  11961  summodc  11962  zsumdc  11963  fsum3  11966  isumz  11968  isumss  11970  fisumss  11971  isumss2  11972  fsum3cvg2  11973  fsumsersdc  11974  fsumsplit  11986  prodeq1f  12131  prodmodclem2a  12155  prodmodclem2  12156  prodmodc  12157  zproddc  12158  fprodseq  12162  prod1dc  12165  prodssdc  12168  fprodssdc  12169  fprodsplitdc  12175  dvdsdc  12377  zdvdsdc  12391  bitsdc  12526  nnmindc  12623  nnminle  12624  uzwodc  12626  nnwosdc  12628  hashdvds  12811  eulerthlemfi  12818  dvdsfi  12829  phisum  12831  infpnlem2  12951  1arith  12958  4sqexercise1  12989  4sqexercise2  12990  4sqlemsdc  12991  ennnfonelemr  13062  ennnfonelemim  13063  ctinf  13069  ctiunctlemudc  13076  ctiunct  13079  ssomct  13084  ssnnctlemct  13085  nninfdclemcl  13087  nninfdclemp1  13089  psrbagfi  14706  psr1clfi  14721  perfectlem2  15743  lgsval  15752  lgsfvalg  15753  lgsfcl2  15754  lgsval2lem  15758  lgsdir2  15781  lgsne0  15786  2lgs  15852  2lgsoddprm  15861  vtxedgfi  16159  vtxlpfi  16160  eupth2lem3lem4fi  16343  sumdc2  16446  bj-charfundcALT  16455  bj-charfunbi  16457  2omap  16645  pw1dceq  16656  nninfsellemdc  16663  iswomninnlem  16705  iswomni0  16707  redcwlpo  16711  redc0  16713  reap0  16714  cndcap  16715  dceqnconst  16716  dcapnconst  16717