Theorem dcbid 786

Description: The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)

Hypothesis

Ref	Expression
dcbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
dcbid	⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒))

Proof of Theorem dcbid

Step	Hyp	Ref	Expression
1		dcbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	notbid 627	. . 3 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
3	1, 2	orbi12d 742	. 2 ⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4		df-dc 781	. 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5		df-dc 781	. 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
6	3, 4, 5	3bitr4g 221	1 ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 103   ∨ wo 664  DECID wdc 780

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665

This theorem depends on definitions:  df-bi 115  df-dc 781

This theorem is referenced by:  exmidexmid  4031  exmidel  4034  dcdifsnid  6263  finexdc  6616  undifdcss  6631  ssfirab  6641  fidcenumlemrks  6660  ltdcpi  6880  enqdc  6918  enqdc1  6919  ltdcnq  6954  fzodcel  9559  exfzdc  9647  sumeq1  10740  sumdc  10743  isummolem2  10768  isummo  10769  zisum  10770  fisum  10774  isumz  10777  isumss  10779  fisumss  10780  isumss2  10781  fisumcvg2  10782  fsum3cvg2  10783  fisumsers  10784  fsumsplit  10797  dvdsdc  11078  zdvdsdc  11091  zsupcllemstep  11215  infssuzex  11219  hashdvds  11471  sumdc2  11654  nninfsellemdc  11857