Theorem dcbii 848

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

Syntax hints:   <-> wb 105  DECID wdc 842

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 619  ax-in2 620  ax-io 717

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

This theorem is referenced by:  dcbi  945  dcned  2409  dfrex2dc  2524  euxfr2dc  2992  exmidexmid  4292  pw1fin  7145  tpfidceq  7165  dcfi  7240  elnn0dc  9906  elnndc  9907  exfzdc  10549  fprod1p  12240  bitsinv1  12603  nnwosdc  12690  prmdc  12782  pclemdc  12941  4sqlemafi  13048  4sqleminfi  13050  4sqexercise1  13051  nninfdclemcl  13149  nninfdclemp1  13151  psr1clfi  14789  nninfsellemdc  16736