Theorem dcbii 842

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 841	. 2 ⊢ ((𝜑 ↔ 𝜓) → (DECID 𝜑 ↔ DECID 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (DECID 𝜑 ↔ DECID 𝜓)

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  2383  dfrex2dc  2498  euxfr2dc  2962  exmidexmid  4248  pw1fin  7022  tpfidceq  7042  dcfi  7098  elnn0dc  9752  elnndc  9753  exfzdc  10391  fprod1p  11985  bitsinv1  12348  nnwosdc  12435  prmdc  12527  pclemdc  12686  4sqlemafi  12793  4sqleminfi  12795  4sqexercise1  12796  nninfdclemcl  12894  nninfdclemp1  12896  psr1clfi  14525  nninfsellemdc  16088