Theorem dcbid 839

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 668	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 794	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 836	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 836	. 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 709  DECID wdc 835

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 615  ax-in2 616  ax-io 710

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

This theorem is referenced by:  dcbiit  840  exmidexmid  4230  exmidel  4239  dcdifsnid  6571  pw2f1odclem  6904  finexdc  6972  pw1dc1  6984  undifdcss  6993  prfidceq  6998  tpfidceq  7000  ssfirab  7006  opabfi  7008  infidc  7009  fidcenumlemrks  7028  dcfi  7056  difinfsnlem  7174  difinfsn  7175  ctssdclemn0  7185  ctssdccl  7186  ctssdclemr  7187  ctssdc  7188  iswomni  7240  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemdc  7252  nninfwlpoim  7253  netap  7337  ltdcpi  7407  enqdc  7445  enqdc1  7446  ltdcnq  7481  fzodcel  10245  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  suprzubdc  10343  nninfdcex  10344  zsupssdc  10345  qdcle  10353  sumeq1  11537  sumdc  11540  summodclem2  11564  summodc  11565  zsumdc  11566  fsum3  11569  isumz  11571  isumss  11573  fisumss  11574  isumss2  11575  fsum3cvg2  11576  fsumsersdc  11577  fsumsplit  11589  prodeq1f  11734  prodmodclem2a  11758  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodseq  11765  prod1dc  11768  prodssdc  11771  fprodssdc  11772  fprodsplitdc  11778  dvdsdc  11980  zdvdsdc  11994  bitsdc  12129  nnmindc  12226  nnminle  12227  uzwodc  12229  nnwosdc  12231  hashdvds  12414  eulerthlemfi  12421  dvdsfi  12432  phisum  12434  infpnlem2  12554  1arith  12561  4sqexercise1  12592  4sqexercise2  12593  4sqlemsdc  12594  ennnfonelemr  12665  ennnfonelemim  12666  ctinf  12672  ctiunctlemudc  12679  ctiunct  12682  ssomct  12687  ssnnctlemct  12688  nninfdclemcl  12690  nninfdclemp1  12692  psr1clfi  14316  perfectlem2  15320  lgsval  15329  lgsfvalg  15330  lgsfcl2  15331  lgsval2lem  15335  lgsdir2  15358  lgsne0  15363  2lgs  15429  2lgsoddprm  15438  sumdc2  15529  bj-charfundcALT  15539  bj-charfunbi  15541  2omap  15726  nninfsellemdc  15741  iswomninnlem  15780  iswomni0  15782  redcwlpo  15786  redc0  15788  reap0  15789  cndcap  15790  dceqnconst  15791  dcapnconst  15792