Theorem dcbid 838

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 667	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 793	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 835	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 835	. 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 708  DECID wdc 834

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 614  ax-in2 615  ax-io 709

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

This theorem is referenced by:  dcbiit  839  exmidexmid  4197  exmidel  4206  dcdifsnid  6505  finexdc  6902  pw1dc1  6913  undifdcss  6922  ssfirab  6933  fidcenumlemrks  6952  dcfi  6980  difinfsnlem  7098  difinfsn  7099  ctssdclemn0  7109  ctssdccl  7110  ctssdclemr  7111  ctssdc  7112  iswomni  7163  enwomnilem  7167  nninfdcinf  7169  nninfwlporlem  7171  nninfwlpoimlemdc  7175  nninfwlpoim  7176  netap  7253  ltdcpi  7322  enqdc  7360  enqdc1  7361  ltdcnq  7396  fzodcel  10152  exfzdc  10240  sumeq1  11363  sumdc  11366  summodclem2  11390  summodc  11391  zsumdc  11392  fsum3  11395  isumz  11397  isumss  11399  fisumss  11400  isumss2  11401  fsum3cvg2  11402  fsumsersdc  11403  fsumsplit  11415  prodeq1f  11560  prodmodclem2a  11584  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodseq  11591  prod1dc  11594  prodssdc  11597  fprodssdc  11598  fprodsplitdc  11604  dvdsdc  11805  zdvdsdc  11819  zsupcllemstep  11946  infssuzex  11950  suprzubdc  11953  nninfdcex  11954  zsupssdc  11955  nnmindc  12035  nnminle  12036  uzwodc  12038  nnwosdc  12040  hashdvds  12221  eulerthlemfi  12228  phisum  12240  infpnlem2  12358  1arith  12365  ennnfonelemr  12424  ennnfonelemim  12425  ctinf  12431  ctiunctlemudc  12438  ctiunct  12441  ssomct  12446  ssnnctlemct  12447  nninfdclemcl  12449  nninfdclemp1  12451  lgsval  14408  lgsfvalg  14409  lgsfcl2  14410  lgsval2lem  14414  lgsdir2  14437  lgsne0  14442  sumdc2  14554  bj-charfundcALT  14564  bj-charfunbi  14566  nninfsellemdc  14762  iswomninnlem  14800  iswomni0  14802  redcwlpo  14806  redc0  14808  reap0  14809  dceqnconst  14810  dcapnconst  14811