Theorem dcbii 852

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

This proof depends on syntax axioms:   ↔ wb 105  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117  df-dc 847

This theorem is used by:  dcbi  949  dcned  2426  dfrex2dc  2541  euxfr2dc  3011  exmidexmid  4333  pw1fin  7217  tpfidceq  7237  fissfi  7263  dcfi  7315  fdcf1  7316  f1setfi  7317  elnn0dc  10011  elnndc  10012  exfzdc  10659  fprod1p  12366  bitsinv1  12729  nnwosdc  12816  prmdc  12908  pclemdc  13067  4sqlemafi  13174  4sqleminfi  13176  4sqexercise1  13177  ballotfilemcdc  13223  ballotfilemdifcfi  13225  ballotfilemdifcfz  13227  ballotfilemiex  13244  nninfdclemcl  13339  nninfdclemp1  13341  psr1clfi  15079  wexmiddiffi  17044  nninfsellemdc  17053