Theorem dcbii 845

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

Syntax hints:   ↔ wb 105  DECID wdc 839

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 617  ax-in2 618  ax-io 714

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

This theorem is referenced by:  dcbi  942  dcned  2406  dfrex2dc  2521  euxfr2dc  2989  exmidexmid  4284  pw1fin  7095  tpfidceq  7115  dcfi  7171  elnn0dc  9835  elnndc  9836  exfzdc  10476  fprod1p  12150  bitsinv1  12513  nnwosdc  12600  prmdc  12692  pclemdc  12851  4sqlemafi  12958  4sqleminfi  12960  4sqexercise1  12961  nninfdclemcl  13059  nninfdclemp1  13061  psr1clfi  14692  nninfsellemdc  16548