Theorem dcbii 841

Description: Equivalence property for decidability. Inference form. (Contributed by Jim Kingdon, 28-Mar-2018.)

Hypothesis

Ref	Expression
dcbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
dcbii	⊢ (DECID 𝜑 ↔ DECID 𝜓)

Proof of Theorem dcbii

Step	Hyp	Ref	Expression
1		dcbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		dcbiit 840	. 2 ⊢ ((𝜑 ↔ 𝜓) → (DECID 𝜑 ↔ DECID 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (DECID 𝜑 ↔ DECID 𝜓)

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  2373  dfrex2dc  2488  euxfr2dc  2949  exmidexmid  4229  pw1fin  6971  tpfidceq  6991  dcfi  7047  elnn0dc  9685  elnndc  9686  exfzdc  10316  fprod1p  11764  nnwosdc  12206  prmdc  12298  pclemdc  12457  4sqlemafi  12564  4sqleminfi  12566  4sqexercise1  12567  nninfdclemcl  12665  nninfdclemp1  12667  nninfsellemdc  15654