Theorem dcbid 833

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 662	. . 3 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
3	1, 2	orbi12d 788	. 2 ⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4		df-dc 830	. 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5		df-dc 830	. 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
6	3, 4, 5	3bitr4g 222	1 ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒))

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

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 609  ax-in2 610  ax-io 704

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

This theorem is referenced by:  dcbiit  834  exmidexmid  4182  exmidel  4191  dcdifsnid  6483  finexdc  6880  pw1dc1  6891  undifdcss  6900  ssfirab  6911  fidcenumlemrks  6930  dcfi  6958  difinfsnlem  7076  difinfsn  7077  ctssdclemn0  7087  ctssdccl  7088  ctssdclemr  7089  ctssdc  7090  iswomni  7141  enwomnilem  7145  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemdc  7153  nninfwlpoim  7154  ltdcpi  7285  enqdc  7323  enqdc1  7324  ltdcnq  7359  fzodcel  10108  exfzdc  10196  sumeq1  11318  sumdc  11321  summodclem2  11345  summodc  11346  zsumdc  11347  fsum3  11350  isumz  11352  isumss  11354  fisumss  11355  isumss2  11356  fsum3cvg2  11357  fsumsersdc  11358  fsumsplit  11370  prodeq1f  11515  prodmodclem2a  11539  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodseq  11546  prod1dc  11549  prodssdc  11552  fprodssdc  11553  fprodsplitdc  11559  dvdsdc  11760  zdvdsdc  11774  zsupcllemstep  11900  infssuzex  11904  suprzubdc  11907  nninfdcex  11908  zsupssdc  11909  nnmindc  11989  nnminle  11990  uzwodc  11992  nnwosdc  11994  hashdvds  12175  eulerthlemfi  12182  phisum  12194  infpnlem2  12312  1arith  12319  ennnfonelemr  12378  ennnfonelemim  12379  ctinf  12385  ctiunctlemudc  12392  ctiunct  12395  ssomct  12400  ssnnctlemct  12401  nninfdclemcl  12403  nninfdclemp1  12405  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgsval2lem  13705  lgsdir2  13728  lgsne0  13733  sumdc2  13834  bj-charfundcALT  13844  bj-charfunbi  13846  nninfsellemdc  14043  iswomninnlem  14081  iswomni0  14083  redcwlpo  14087  redc0  14089  reap0  14090  dceqnconst  14091  dcapnconst  14092