Theorem dcbii 836

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

Syntax hints:   <-> wb 104  DECID wdc 830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705

This theorem depends on definitions:  df-bi 116  df-dc 831

This theorem is referenced by:  dcbi  932  dcned  2347  dfrex2dc  2462  euxfr2dc  2916  exmidexmid  4183  pw1fin  6892  dcfi  6962  elnn0dc  9574  elnndc  9575  exfzdc  10200  fprod1p  11566  nnwosdc  11998  prmdc  12088  pclemdc  12246  nninfdclemcl  12407  nninfdclemp1  12409  nninfsellemdc  14128