Theorem dcbii 848

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

Syntax hints:   ↔ wb 105  DECID wdc 842

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 619  ax-in2 620  ax-io 717

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

This theorem is referenced by:  dcbi  945  dcned  2409  dfrex2dc  2524  euxfr2dc  2992  exmidexmid  4292  pw1fin  7145  tpfidceq  7165  dcfi  7223  elnn0dc  9889  elnndc  9890  exfzdc  10532  fprod1p  12223  bitsinv1  12586  nnwosdc  12673  prmdc  12765  pclemdc  12924  4sqlemafi  13031  4sqleminfi  13033  4sqexercise1  13034  nninfdclemcl  13132  nninfdclemp1  13134  psr1clfi  14772  nninfsellemdc  16719