Theorem dcbid 846

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

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 717

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

This theorem is referenced by:  dcbiit  847  exmidexmid  4292  exmidel  4301  suppssdc  6438  dcdifsnid  6715  pw2f1odclem  7063  finexdc  7135  elssdc  7137  eqsndc  7138  pw1dc1  7149  undifdcss  7158  prfidceq  7163  tpfidceq  7165  ssfirab  7172  opabfi  7175  infidc  7176  fidcenumlemrks  7195  dcfi  7240  difinfsnlem  7358  difinfsn  7359  ctssdclemn0  7369  ctssdccl  7370  ctssdclemr  7371  ctssdc  7372  iswomni  7424  enwomnilem  7428  nninfdcinf  7430  nninfwlporlem  7432  nninfwlpoimlemdc  7436  nninfinfwlpolem  7437  nninfwlpoim  7438  nninfinfwlpo  7439  netap  7533  ltdcpi  7603  enqdc  7641  enqdc1  7642  ltdcnq  7677  fzodcel  10450  exfzdc  10549  zsupcllemstep  10552  infssuzex  10556  suprzubdc  10559  nninfdcex  10560  zsupssdc  10561  qdcle  10569  fzowrddc  11294  sumeq1  11995  sumdc  11998  summodclem2  12023  summodc  12024  zsumdc  12025  fsum3  12028  isumz  12030  isumss  12032  fisumss  12033  isumss2  12034  fsum3cvg2  12035  fsumsersdc  12036  fsumsplit  12048  prodeq1f  12193  prodmodclem2a  12217  prodmodclem2  12218  prodmodc  12219  zproddc  12220  fprodseq  12224  prod1dc  12227  prodssdc  12230  fprodssdc  12231  fprodsplitdc  12237  dvdsdc  12439  zdvdsdc  12453  bitsdc  12588  nnmindc  12685  nnminle  12686  uzwodc  12688  nnwosdc  12690  hashdvds  12873  eulerthlemfi  12880  dvdsfi  12891  phisum  12893  infpnlem2  13013  1arith  13020  4sqexercise1  13051  4sqexercise2  13052  4sqlemsdc  13053  ennnfonelemr  13124  ennnfonelemim  13125  ctinf  13131  ctiunctlemudc  13138  ctiunct  13141  ssomct  13146  ssnnctlemct  13147  nninfdclemcl  13149  nninfdclemp1  13151  psrbagfi  14770  psrbaglecl  14771  psrbagcon  14772  psr1clfi  14789  perfectlem2  15814  lgsval  15823  lgsfvalg  15824  lgsfcl2  15825  lgsval2lem  15829  lgsdir2  15852  lgsne0  15857  2lgs  15923  2lgsoddprm  15932  vtxedgfi  16230  vtxlpfi  16231  eupth2lem3lem4fi  16414  sumdc2  16517  bj-charfundcALT  16525  bj-charfunbi  16527  2omap  16715  pw1dceq  16726  nninfsellemdc  16736  iswomninnlem  16782  iswomni0  16784  redcwlpo  16788  redc0  16790  reap0  16791  cndcap  16792  dceqnconst  16793  dcapnconst  16794