Theorem dcbii 848

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

Syntax hints:   ↔ wb 105  DECID wdc 842

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 717

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

This theorem is referenced by:  dcbi  945  dcned  2420  dfrex2dc  2535  euxfr2dc  3005  exmidexmid  4314  pw1fin  7183  tpfidceq  7203  fissfi  7229  dcfi  7281  elnn0dc  9961  elnndc  9962  exfzdc  10608  fprod1p  12310  bitsinv1  12673  nnwosdc  12760  prmdc  12852  pclemdc  13011  4sqlemafi  13118  4sqleminfi  13120  4sqexercise1  13121  ballotfilemcdc  13167  ballotfilemdifcfi  13169  ballotfilemdifcfz  13171  ballotfilemiex  13188  nninfdclemcl  13283  nninfdclemp1  13285  psr1clfi  14969  nninfsellemdc  16914