Theorem dcbid 824

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 657	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 783	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 821	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 821	. 2 |- (DECID ch <-> ( ch \/ -. ch ) )
6	3, 4, 5	3bitr4g 222	1 |- ( ph -> (DECID ps <-> DECID ch ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   \/ wo 698  DECID wdc 820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116  df-dc 821

This theorem is referenced by:  dcbiit  825  exmidexmid  4128  exmidel  4136  dcdifsnid  6408  finexdc  6804  undifdcss  6819  ssfirab  6830  fidcenumlemrks  6849  difinfsnlem  6992  difinfsn  6993  ctssdclemn0  7003  ctssdccl  7004  ctssdclemr  7005  ctssdc  7006  iswomni  7047  enwomnilem  7050  ltdcpi  7155  enqdc  7193  enqdc1  7194  ltdcnq  7229  fzodcel  9960  exfzdc  10048  sumeq1  11156  sumdc  11159  summodclem2  11183  summodc  11184  zsumdc  11185  fsum3  11188  isumz  11190  isumss  11192  fisumss  11193  isumss2  11194  fsum3cvg2  11195  fsumsersdc  11196  fsumsplit  11208  prodeq1f  11353  prodmodclem2a  11377  prodmodclem2  11378  prodmodc  11379  zproddc  11380  fprodseq  11384  dvdsdc  11537  zdvdsdc  11550  zsupcllemstep  11674  infssuzex  11678  hashdvds  11933  ennnfonelemr  11972  ennnfonelemim  11973  ctinf  11979  ctiunctlemudc  11986  ctiunct  11989  sumdc2  13177  nninfsellemdc  13381  iswomninnlem  13417  redcwlpo  13422  dceqnconst  13423