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  2418  dfrex2dc  2533  euxfr2dc  3002  exmidexmid  4309  pw1fin  7170  tpfidceq  7190  fissfi  7216  dcfi  7268  elnn0dc  9943  elnndc  9944  exfzdc  10586  fprod1p  12285  bitsinv1  12648  nnwosdc  12735  prmdc  12827  pclemdc  12986  4sqlemafi  13093  4sqleminfi  13095  4sqexercise1  13096  nninfdclemcl  13199  nninfdclemp1  13201  psr1clfi  14843  nninfsellemdc  16788