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  6671  pw2f1odclem  7019  finexdc  7091  elssdc  7093  eqsndc  7094  pw1dc1  7105  undifdcss  7114  prfidceq  7119  tpfidceq  7121  ssfirab  7128  opabfi  7131  infidc  7132  fidcenumlemrks  7151  dcfi  7179  difinfsnlem  7297  difinfsn  7298  ctssdclemn0  7308  ctssdccl  7309  ctssdclemr  7310  ctssdc  7311  iswomni  7363  enwomnilem  7367  nninfdcinf  7369  nninfwlporlem  7371  nninfwlpoimlemdc  7375  nninfinfwlpolem  7376  nninfwlpoim  7377  nninfinfwlpo  7378  netap  7472  ltdcpi  7542  enqdc  7580  enqdc1  7581  ltdcnq  7616  fzodcel  10387  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  suprzubdc  10495  nninfdcex  10496  zsupssdc  10497  qdcle  10505  fzowrddc  11227  sumeq1  11915  sumdc  11918  summodclem2  11942  summodc  11943  zsumdc  11944  fsum3  11947  isumz  11949  isumss  11951  fisumss  11952  isumss2  11953  fsum3cvg2  11954  fsumsersdc  11955  fsumsplit  11967  prodeq1f  12112  prodmodclem2a  12136  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodseq  12143  prod1dc  12146  prodssdc  12149  fprodssdc  12150  fprodsplitdc  12156  dvdsdc  12358  zdvdsdc  12372  bitsdc  12507  nnmindc  12604  nnminle  12605  uzwodc  12607  nnwosdc  12609  hashdvds  12792  eulerthlemfi  12799  dvdsfi  12810  phisum  12812  infpnlem2  12932  1arith  12939  4sqexercise1  12970  4sqexercise2  12971  4sqlemsdc  12972  ennnfonelemr  13043  ennnfonelemim  13044  ctinf  13050  ctiunctlemudc  13057  ctiunct  13060  ssomct  13065  ssnnctlemct  13066  nninfdclemcl  13068  nninfdclemp1  13070  psrbagfi  14686  psr1clfi  14701  perfectlem2  15723  lgsval  15732  lgsfvalg  15733  lgsfcl2  15734  lgsval2lem  15738  lgsdir2  15761  lgsne0  15766  2lgs  15832  2lgsoddprm  15841  vtxedgfi  16139  vtxlpfi  16140  sumdc2  16395  bj-charfundcALT  16404  bj-charfunbi  16406  2omap  16594  pw1dceq  16605  nninfsellemdc  16612  iswomninnlem  16653  iswomni0  16655  redcwlpo  16659  redc0  16661  reap0  16662  cndcap  16663  dceqnconst  16664  dcapnconst  16665