Theorem dcbii 842

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

Syntax hints:   <-> wb 105  DECID wdc 836

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 615  ax-in2 616  ax-io 711

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

This theorem is referenced by:  dcbi  939  dcned  2382  dfrex2dc  2497  euxfr2dc  2958  exmidexmid  4240  pw1fin  7007  tpfidceq  7027  dcfi  7083  elnn0dc  9732  elnndc  9733  exfzdc  10369  fprod1p  11910  bitsinv1  12273  nnwosdc  12360  prmdc  12452  pclemdc  12611  4sqlemafi  12718  4sqleminfi  12720  4sqexercise1  12721  nninfdclemcl  12819  nninfdclemp1  12821  psr1clfi  14450  nninfsellemdc  15947