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  4241  pw1fin  7009  tpfidceq  7029  dcfi  7085  elnn0dc  9734  elnndc  9735  exfzdc  10371  fprod1p  11943  bitsinv1  12306  nnwosdc  12393  prmdc  12485  pclemdc  12644  4sqlemafi  12751  4sqleminfi  12753  4sqexercise1  12754  nninfdclemcl  12852  nninfdclemp1  12854  psr1clfi  14483  nninfsellemdc  15984