Theorem dcbii 830

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

Syntax hints:   <-> wb 104  DECID wdc 824

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 604  ax-in2 605  ax-io 699

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

This theorem is referenced by:  dcbi  926  dcned  2341  dfrex2dc  2456  euxfr2dc  2910  exmidexmid  4174  pw1fin  6872  dcfi  6942  elnn0dc  9545  elnndc  9546  exfzdc  10171  fprod1p  11536  nnwosdc  11968  prmdc  12058  pclemdc  12216  nninfdclemcl  12377  nninfdclemp1  12379  nninfsellemdc  13850