Theorem dcbid 823

Description: Equivalence property for decidability. Deduction form. (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 656	. . 3 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
3	1, 2	orbi12d 782	. 2 ⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4		df-dc 820	. 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5		df-dc 820	. 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
6	3, 4, 5	3bitr4g 222	1 ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   ∨ wo 697  DECID wdc 819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698

This theorem depends on definitions:  df-bi 116  df-dc 820

This theorem is referenced by:  dcbiit  824  exmidexmid  4115  exmidel  4123  dcdifsnid  6393  finexdc  6789  undifdcss  6804  ssfirab  6815  fidcenumlemrks  6834  difinfsnlem  6977  difinfsn  6978  ctssdclemn0  6988  ctssdccl  6989  ctssdclemr  6990  ctssdc  6991  ltdcpi  7124  enqdc  7162  enqdc1  7163  ltdcnq  7198  fzodcel  9922  exfzdc  10010  sumeq1  11117  sumdc  11120  summodclem2  11144  summodc  11145  zsumdc  11146  fsum3  11149  isumz  11151  isumss  11153  fisumss  11154  isumss2  11155  fsum3cvg2  11156  fsumsersdc  11157  fsumsplit  11169  prodeq1f  11314  dvdsdc  11490  zdvdsdc  11503  zsupcllemstep  11627  infssuzex  11631  hashdvds  11886  ennnfonelemr  11925  ennnfonelemim  11926  ctinf  11932  ctiunctlemudc  11939  ctiunct  11942  sumdc2  12995  nninfsellemdc  13195