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  6672  pw2f1odclem  7020  finexdc  7092  elssdc  7094  eqsndc  7095  pw1dc1  7106  undifdcss  7115  prfidceq  7120  tpfidceq  7122  ssfirab  7129  opabfi  7132  infidc  7133  fidcenumlemrks  7152  dcfi  7180  difinfsnlem  7298  difinfsn  7299  ctssdclemn0  7309  ctssdccl  7310  ctssdclemr  7311  ctssdc  7312  iswomni  7364  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemdc  7376  nninfinfwlpolem  7377  nninfwlpoim  7378  nninfinfwlpo  7379  netap  7473  ltdcpi  7543  enqdc  7581  enqdc1  7582  ltdcnq  7617  fzodcel  10388  exfzdc  10486  zsupcllemstep  10489  infssuzex  10493  suprzubdc  10496  nninfdcex  10497  zsupssdc  10498  qdcle  10506  fzowrddc  11228  sumeq1  11916  sumdc  11919  summodclem2  11944  summodc  11945  zsumdc  11946  fsum3  11949  isumz  11951  isumss  11953  fisumss  11954  isumss2  11955  fsum3cvg2  11956  fsumsersdc  11957  fsumsplit  11969  prodeq1f  12114  prodmodclem2a  12138  prodmodclem2  12139  prodmodc  12140  zproddc  12141  fprodseq  12145  prod1dc  12148  prodssdc  12151  fprodssdc  12152  fprodsplitdc  12158  dvdsdc  12360  zdvdsdc  12374  bitsdc  12509  nnmindc  12606  nnminle  12607  uzwodc  12609  nnwosdc  12611  hashdvds  12794  eulerthlemfi  12801  dvdsfi  12812  phisum  12814  infpnlem2  12934  1arith  12941  4sqexercise1  12972  4sqexercise2  12973  4sqlemsdc  12974  ennnfonelemr  13045  ennnfonelemim  13046  ctinf  13052  ctiunctlemudc  13059  ctiunct  13062  ssomct  13067  ssnnctlemct  13068  nninfdclemcl  13070  nninfdclemp1  13072  psrbagfi  14689  psr1clfi  14704  perfectlem2  15726  lgsval  15735  lgsfvalg  15736  lgsfcl2  15737  lgsval2lem  15741  lgsdir2  15764  lgsne0  15769  2lgs  15835  2lgsoddprm  15844  vtxedgfi  16142  vtxlpfi  16143  sumdc2  16398  bj-charfundcALT  16407  bj-charfunbi  16409  2omap  16597  pw1dceq  16608  nninfsellemdc  16615  iswomninnlem  16656  iswomni0  16658  redcwlpo  16662  redc0  16664  reap0  16665  cndcap  16666  dceqnconst  16667  dcapnconst  16668