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  2381  dfrex2dc  2496  euxfr2dc  2957  exmidexmid  4239  pw1fin  6989  tpfidceq  7009  dcfi  7065  elnn0dc  9714  elnndc  9715  exfzdc  10350  fprod1p  11829  bitsinv1  12192  nnwosdc  12279  prmdc  12371  pclemdc  12530  4sqlemafi  12637  4sqleminfi  12639  4sqexercise1  12640  nninfdclemcl  12738  nninfdclemp1  12740  psr1clfi  14368  nninfsellemdc  15811