Theorem dcbii 847

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

Syntax hints:   ↔ wb 105  DECID wdc 841

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 716

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

This theorem is referenced by:  dcbi  944  dcned  2408  dfrex2dc  2523  euxfr2dc  2991  exmidexmid  4286  pw1fin  7101  tpfidceq  7121  dcfi  7179  elnn0dc  9844  elnndc  9845  exfzdc  10485  fprod1p  12159  bitsinv1  12522  nnwosdc  12609  prmdc  12701  pclemdc  12860  4sqlemafi  12967  4sqleminfi  12969  4sqexercise1  12970  nninfdclemcl  13068  nninfdclemp1  13070  psr1clfi  14701  nninfsellemdc  16612