Theorem dcbid 787

Description: The equivalent of a decidable proposition is decidable. (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 628	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 743	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 782	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 782	. 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 665  DECID wdc 781

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

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

This theorem is referenced by:  exmidexmid  4039  exmidel  4044  dcdifsnid  6279  finexdc  6674  undifdcss  6689  ssfirab  6699  fidcenumlemrks  6718  ltdcpi  6945  enqdc  6983  enqdc1  6984  ltdcnq  7019  fzodcel  9626  exfzdc  9714  sumeq1  10807  sumdc  10810  isummolem2  10835  isummo  10836  zisum  10837  fisum  10841  isumz  10844  isumss  10846  fisumss  10847  isumss2  10848  fisumcvg2  10849  fsum3cvg2  10850  fisumsers  10851  fsumsplit  10864  dvdsdc  11145  zdvdsdc  11158  zsupcllemstep  11282  infssuzex  11286  hashdvds  11538  sumdc2  12003  nninfsellemdc  12205