Theorem dcbii 842

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 841	. 2 |- ( ( ph <-> ps ) -> (DECID ph <-> DECID ps ) )
3	1, 2	ax-mp 5	1 |- (DECID ph <-> DECID ps )

Syntax hints:   <-> wb 105  DECID wdc 836

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 615  ax-in2 616  ax-io 711

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

This theorem is referenced by:  dcbi  939  dcned  2384  dfrex2dc  2499  euxfr2dc  2965  exmidexmid  4256  pw1fin  7033  tpfidceq  7053  dcfi  7109  elnn0dc  9767  elnndc  9768  exfzdc  10406  fprod1p  12025  bitsinv1  12388  nnwosdc  12475  prmdc  12567  pclemdc  12726  4sqlemafi  12833  4sqleminfi  12835  4sqexercise1  12836  nninfdclemcl  12934  nninfdclemp1  12936  psr1clfi  14565  nninfsellemdc  16149