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  10020  elnndc  10021  exfzdc  10669  fprod1p  12382  bitsinv1  12745  nnwosdc  12832  prmdc  12924  pclemdc  13087  4sqlemafi  13194  4sqleminfi  13196  4sqexercise1  13197  ballotfilemcdc  13272  ballotfilemdifcfi  13274  ballotfilemdifcfz  13276  ballotfilemiex  13293  nninfdclemcl  13388  nninfdclemp1  13390  psr1clfi  15128  ppiqfi  16158  prmdvdsfi  16159  ppiprm  16170  ppidif  16175  ppiqub  16194  wexmiddiffi  17142  nninfsellemdc  17151