Theorem dcbii 852

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

This proof depends on syntax axioms:   <-> wb 105  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117  df-dc 847

This theorem is used by:  dcbi  949  dcned  2426  dfrex2dc  2541  euxfr2dc  3011  exmidexmid  4335  pw1fin  7221  tpfidceq  7241  fissfi  7267  dcfi  7320  fdcf1  7321  f1setfi  7322  elnn0dc  10027  elnndc  10028  exfzdc  10676  fprod1p  12391  bitsinv1  12754  nnwosdc  12841  prmdc  12933  pclemdc  13096  4sqlemafi  13203  4sqleminfi  13205  4sqexercise1  13206  ballotfilemcdc  13281  ballotfilemdifcfi  13283  ballotfilemdifcfz  13285  ballotfilemiex  13302  nninfdclemcl  13397  nninfdclemp1  13399  gsummptfidmsplit  14254  psr1clfi  15198  ppiqfi  16242  prmdvdsfi  16243  ppiprm  16259  chtprm  16261  chtdif  16264  efchtqdvds  16265  ppidif  16269  prmorcht  16282  ppiqub  16293  bpos  16320  wexmiddiffi  17249  nninfsellemdc  17259