Theorem dcbid 823

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 656	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 782	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 820	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 820	. 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 697  DECID wdc 819

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 603  ax-in2 604  ax-io 698

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

This theorem is referenced by:  dcbiit  824  exmidexmid  4120  exmidel  4128  dcdifsnid  6400  finexdc  6796  undifdcss  6811  ssfirab  6822  fidcenumlemrks  6841  difinfsnlem  6984  difinfsn  6985  ctssdclemn0  6995  ctssdccl  6996  ctssdclemr  6997  ctssdc  6998  ltdcpi  7131  enqdc  7169  enqdc1  7170  ltdcnq  7205  fzodcel  9929  exfzdc  10017  sumeq1  11124  sumdc  11127  summodclem2  11151  summodc  11152  zsumdc  11153  fsum3  11156  isumz  11158  isumss  11160  fisumss  11161  isumss2  11162  fsum3cvg2  11163  fsumsersdc  11164  fsumsplit  11176  prodeq1f  11321  prodmodclem2a  11345  prodmodclem2  11346  prodmodc  11347  dvdsdc  11501  zdvdsdc  11514  zsupcllemstep  11638  infssuzex  11642  hashdvds  11897  ennnfonelemr  11936  ennnfonelemim  11937  ctinf  11943  ctiunctlemudc  11950  ctiunct  11953  sumdc2  13006  nninfsellemdc  13206