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  7223  tpfidceq  7243  fissfi  7269  dcfi  7320  fdcf1  7321  f1setfi  7322  elnn0dc  10026  elnndc  10027  exfzdc  10675  fprod1p  12390  bitsinv1  12753  nnwosdc  12840  prmdc  12932  pclemdc  13095  4sqlemafi  13202  4sqleminfi  13204  4sqexercise1  13205  ballotfilemcdc  13280  ballotfilemdifcfi  13282  ballotfilemdifcfz  13284  ballotfilemiex  13301  nninfdclemcl  13396  nninfdclemp1  13398  gsummptfidmsplit  14253  psr1clfi  15207  ppiqfi  16259  prmdvdsfi  16260  ppiprm  16276  chtprm  16278  chtdif  16281  efchtqdvds  16282  ppidif  16286  prmorcht  16299  ppiqub  16310  bpos  16337  wexmiddiffi  17266  nninfsellemdc  17276