Theorem dcbii 841

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

Syntax hints:   <-> wb 105  DECID wdc 835

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 710

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

This theorem is referenced by:  dcbi  938  dcned  2370  dfrex2dc  2485  euxfr2dc  2946  exmidexmid  4226  pw1fin  6968  dcfi  7042  elnn0dc  9679  elnndc  9680  exfzdc  10310  fprod1p  11745  nnwosdc  12179  prmdc  12271  pclemdc  12429  4sqlemafi  12536  4sqleminfi  12538  4sqexercise1  12539  nninfdclemcl  12608  nninfdclemp1  12610  nninfsellemdc  15570