Theorem dcbii 840

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

Syntax hints:   <-> wb 105  DECID wdc 834

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 614  ax-in2 615  ax-io 709

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

This theorem is referenced by:  dcbi  936  dcned  2353  dfrex2dc  2468  euxfr2dc  2923  exmidexmid  4197  pw1fin  6910  dcfi  6980  elnn0dc  9611  elnndc  9612  exfzdc  10240  fprod1p  11607  nnwosdc  12040  prmdc  12130  pclemdc  12288  nninfdclemcl  12449  nninfdclemp1  12451  nninfsellemdc  14762