Theorem dcbii 845

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

Syntax hints:   <-> wb 105  DECID wdc 839

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 617  ax-in2 618  ax-io 714

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

This theorem is referenced by:  dcbi  942  dcned  2406  dfrex2dc  2521  euxfr2dc  2988  exmidexmid  4280  pw1fin  7083  tpfidceq  7103  dcfi  7159  elnn0dc  9818  elnndc  9819  exfzdc  10458  fprod1p  12126  bitsinv1  12489  nnwosdc  12576  prmdc  12668  pclemdc  12827  4sqlemafi  12934  4sqleminfi  12936  4sqexercise1  12937  nninfdclemcl  13035  nninfdclemp1  13037  psr1clfi  14668  nninfsellemdc  16464