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  10021  elnndc  10022  exfzdc  10670  fprod1p  12385  bitsinv1  12748  nnwosdc  12835  prmdc  12927  pclemdc  13090  4sqlemafi  13197  4sqleminfi  13199  4sqexercise1  13200  ballotfilemcdc  13275  ballotfilemdifcfi  13277  ballotfilemdifcfz  13279  ballotfilemiex  13296  nninfdclemcl  13391  nninfdclemp1  13393  psr1clfi  15170  ppiqfi  16203  prmdvdsfi  16204  ppiprm  16220  chtprm  16222  chtdif  16225  efchtqdvds  16226  ppidif  16230  prmorcht  16243  ppiqub  16254  bpos  16281  wexmiddiffi  17210  nninfsellemdc  17219