Theorem dcbid 843

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 671	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 798	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 840	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 840	. 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 713  DECID wdc 839

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 617  ax-in2 618  ax-io 714

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

This theorem is referenced by:  dcbiit  844  exmidexmid  4284  exmidel  4293  dcdifsnid  6667  pw2f1odclem  7015  finexdc  7085  elssdc  7087  eqsndc  7088  pw1dc1  7099  undifdcss  7108  prfidceq  7113  tpfidceq  7115  ssfirab  7121  opabfi  7123  infidc  7124  fidcenumlemrks  7143  dcfi  7171  difinfsnlem  7289  difinfsn  7290  ctssdclemn0  7300  ctssdccl  7301  ctssdclemr  7302  ctssdc  7303  iswomni  7355  enwomnilem  7359  nninfdcinf  7361  nninfwlporlem  7363  nninfwlpoimlemdc  7367  nninfinfwlpolem  7368  nninfwlpoim  7369  nninfinfwlpo  7370  netap  7463  ltdcpi  7533  enqdc  7571  enqdc1  7572  ltdcnq  7607  fzodcel  10378  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  suprzubdc  10486  nninfdcex  10487  zsupssdc  10488  qdcle  10496  fzowrddc  11218  sumeq1  11906  sumdc  11909  summodclem2  11933  summodc  11934  zsumdc  11935  fsum3  11938  isumz  11940  isumss  11942  fisumss  11943  isumss2  11944  fsum3cvg2  11945  fsumsersdc  11946  fsumsplit  11958  prodeq1f  12103  prodmodclem2a  12127  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodseq  12134  prod1dc  12137  prodssdc  12140  fprodssdc  12141  fprodsplitdc  12147  dvdsdc  12349  zdvdsdc  12363  bitsdc  12498  nnmindc  12595  nnminle  12596  uzwodc  12598  nnwosdc  12600  hashdvds  12783  eulerthlemfi  12790  dvdsfi  12801  phisum  12803  infpnlem2  12923  1arith  12930  4sqexercise1  12961  4sqexercise2  12962  4sqlemsdc  12963  ennnfonelemr  13034  ennnfonelemim  13035  ctinf  13041  ctiunctlemudc  13048  ctiunct  13051  ssomct  13056  ssnnctlemct  13057  nninfdclemcl  13059  nninfdclemp1  13061  psrbagfi  14677  psr1clfi  14692  perfectlem2  15714  lgsval  15723  lgsfvalg  15724  lgsfcl2  15725  lgsval2lem  15729  lgsdir2  15752  lgsne0  15757  2lgs  15823  2lgsoddprm  15832  vtxedgfi  16095  vtxlpfi  16096  sumdc2  16331  bj-charfundcALT  16340  bj-charfunbi  16342  2omap  16530  pw1dceq  16541  nninfsellemdc  16548  iswomninnlem  16589  iswomni0  16591  redcwlpo  16595  redc0  16597  reap0  16598  cndcap  16599  dceqnconst  16600  dcapnconst  16601