Theorem dcbid 850

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 720  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117  df-dc 847

This theorem is used by:  dcbiit  851  ifeqeqxdc  3687  exmidexmid  4333  exmidel  4342  suppssdc  6500  dcdifsnid  6777  pw2f1odclem  7134  finexdc  7207  elssdc  7209  eqsndc  7210  pw1dc1  7221  undifdcss  7230  prfidceq  7235  tpfidceq  7237  ssfirab  7244  opabfi  7247  infidc  7248  fissfi  7263  fidcenumlemrks  7270  dcfi  7315  2omap  7318  difinfsnlem  7439  difinfsn  7440  ctssdclemn0  7450  ctssdccl  7451  ctssdclemr  7452  ctssdc  7453  iswomni  7505  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemdc  7517  nninfinfwlpolem  7518  nninfwlpoim  7519  nninfinfwlpo  7520  netap  7620  ltdcpi  7690  enqdc  7728  enqdc1  7729  ltdcnq  7764  indfdc  9300  fzodcel  10570  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  suprzubdc  10681  nninfdcex  10682  zsupssdc  10683  qdcle  10691  nn0sqdc  11160  hashfibclem  11296  fzowrddc  11433  sumeq1  12137  sumdc  12140  summodclem2  12165  summodc  12166  zsumdc  12167  fsum3  12170  isumz  12172  isumss  12174  fisumss  12175  isumss2  12176  fsum3cvg2  12177  fsumsersdc  12178  fsumsplit  12190  prodeq1f  12335  prodmodclem2a  12359  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodseq  12366  prod1dc  12369  prodssdc  12372  fprodssdc  12373  fprodsplitdc  12379  dvdsdc  12581  zdvdsdc  12595  bitsdc  12730  nnmindc  12827  nnminle  12828  uzwodc  12830  nnwosdc  12832  hashdvds  13019  eulerthlemfi  13026  dvdsfi  13037  phisum  13039  infpnlem2  13159  1arith  13166  4sqexercise1  13197  4sqexercise2  13198  4sqlemsdc  13199  ballotfilemcdc  13272  ballotfilemdifcfz  13276  ballotfilemefi  13286  ennnfonelemr  13363  ennnfonelemim  13364  ctinf  13370  ctiunctlemudc  13377  ctiunct  13380  ssomct  13385  ssnnctlemct  13386  nninfdclemcl  13388  nninfdclemp1  13390  psrbagfi  15108  psrbaglecl  15109  psrbagcon  15111  psr1clfi  15128  ppiqub  16194  perfectlem2  16198  lgsval  16221  lgsfvalg  16222  lgsfcl2  16223  lgsval2lem  16227  lgsdir2  16250  lgsne0  16255  2lgs  16321  2lgsoddprm  16330  vtxedgfi  16628  vtxlpfi  16629  eupth2lem3lem4fi  16812  sumdc2  16925  bj-charfundcALT  16933  bj-charfunbi  16935  pw1dceq  17133  nninfsellemdc  17151  iswomninnlem  17197  iswomni0  17199  redcwlpo  17203  redc0  17205  reap0  17206  cndcap  17207  dceqnconst  17208  dcapnconst  17209