Theorem dcbid 838

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 667	. . 3 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
3	1, 2	orbi12d 793	. 2 ⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4		df-dc 835	. 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5		df-dc 835	. 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 708  DECID wdc 834

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 614  ax-in2 615  ax-io 709

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

This theorem is referenced by:  dcbiit  839  exmidexmid  4196  exmidel  4205  dcdifsnid  6504  finexdc  6901  pw1dc1  6912  undifdcss  6921  ssfirab  6932  fidcenumlemrks  6951  dcfi  6979  difinfsnlem  7097  difinfsn  7098  ctssdclemn0  7108  ctssdccl  7109  ctssdclemr  7110  ctssdc  7111  iswomni  7162  enwomnilem  7166  nninfdcinf  7168  nninfwlporlem  7170  nninfwlpoimlemdc  7174  nninfwlpoim  7175  netap  7252  ltdcpi  7321  enqdc  7359  enqdc1  7360  ltdcnq  7395  fzodcel  10151  exfzdc  10239  sumeq1  11362  sumdc  11365  summodclem2  11389  summodc  11390  zsumdc  11391  fsum3  11394  isumz  11396  isumss  11398  fisumss  11399  isumss2  11400  fsum3cvg2  11401  fsumsersdc  11402  fsumsplit  11414  prodeq1f  11559  prodmodclem2a  11583  prodmodclem2  11584  prodmodc  11585  zproddc  11586  fprodseq  11590  prod1dc  11593  prodssdc  11596  fprodssdc  11597  fprodsplitdc  11603  dvdsdc  11804  zdvdsdc  11818  zsupcllemstep  11945  infssuzex  11949  suprzubdc  11952  nninfdcex  11953  zsupssdc  11954  nnmindc  12034  nnminle  12035  uzwodc  12037  nnwosdc  12039  hashdvds  12220  eulerthlemfi  12227  phisum  12239  infpnlem2  12357  1arith  12364  ennnfonelemr  12423  ennnfonelemim  12424  ctinf  12430  ctiunctlemudc  12437  ctiunct  12440  ssomct  12445  ssnnctlemct  12446  nninfdclemcl  12448  nninfdclemp1  12450  lgsval  14375  lgsfvalg  14376  lgsfcl2  14377  lgsval2lem  14381  lgsdir2  14404  lgsne0  14409  sumdc2  14521  bj-charfundcALT  14531  bj-charfunbi  14533  nninfsellemdc  14729  iswomninnlem  14767  iswomni0  14769  redcwlpo  14773  redc0  14775  reap0  14776  dceqnconst  14777  dcapnconst  14778