Theorem dcbii 852

Description: Equivalence property for decidability. Inference form. (Contributed by Jim Kingdon, 28-Mar-2018.)

Hypothesis

Ref	Expression
dcbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
dcbii	|- (DECID ph <-> DECID ps )

Proof of Theorem dcbii

Step	Hyp	Ref	Expression
1		dcbii.1	. 2 |- ( ph <-> ps )
2		dcbiit 851	. 2 |- ( ( ph <-> ps ) -> (DECID ph <-> DECID ps ) )
3	1, 2	ax-mp 5	1 |- (DECID ph <-> DECID ps )

Syntax hints:   <-> wb 105  DECID wdc 846

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 623  ax-in2 624  ax-io 721

This theorem depends on definitions:  df-bi 117  df-dc 847

This theorem is referenced by:  dcbi  949  dcned  2426  dfrex2dc  2541  euxfr2dc  3011  exmidexmid  4328  pw1fin  7207  tpfidceq  7227  fissfi  7253  dcfi  7305  fdcf1  7306  f1setfi  7307  elnn0dc  9990  elnndc  9991  exfzdc  10637  fprod1p  12344  bitsinv1  12707  nnwosdc  12794  prmdc  12886  pclemdc  13045  4sqlemafi  13152  4sqleminfi  13154  4sqexercise1  13155  ballotfilemcdc  13201  ballotfilemdifcfi  13203  ballotfilemdifcfz  13205  ballotfilemiex  13222  nninfdclemcl  13317  nninfdclemp1  13319  psr1clfi  15002  nninfsellemdc  16958