Theorem dcbid 782

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 625	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 740	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 777	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 777	. 2 |- (DECID ch <-> ( ch \/ -. ch ) )
6	3, 4, 5	3bitr4g 221	1 |- ( ph -> (DECID ps <-> DECID ch ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 103   \/ wo 662  DECID wdc 776

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663

This theorem depends on definitions:  df-bi 115  df-dc 777

This theorem is referenced by:  exmidexmid  3987  exmidel  3990  dcdifsnid  6166  undifdcss  6467  ssfirab  6475  ltdcpi  6627  enqdc  6665  enqdc1  6666  ltdcnq  6701  exfzdc  9378  sumeq1  10393  sumdc  10396  dvdsdc  10411  zdvdsdc  10424  zsupcllemstep  10548  infssuzex  10552  hashdvds  10804  sumdc2  10869