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  4335  exmidel  4344  suppssdc  6504  suppinisegdc  6513  dcdifsnid  6782  pw2f1odclem  7140  finexdc  7213  elssdc  7215  eqsndc  7216  pw1dc1  7227  undifdcss  7236  prfidceq  7241  tpfidceq  7243  ssfirab  7250  opabfi  7253  infidc  7254  fissfi  7269  relresfin  7270  fidcenumlemrks  7277  funisfsuppdc  7298  dcfi  7320  ofrfidc  7323  2omap  7324  difinfsnlem  7445  difinfsn  7446  ctssdclemn0  7456  ctssdccl  7457  ctssdclemr  7458  ctssdc  7459  iswomni  7511  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemdc  7523  nninfinfwlpolem  7524  nninfwlpoim  7525  nninfinfwlpo  7526  netap  7626  ltdcpi  7696  enqdc  7734  enqdc1  7735  ltdcnq  7770  indfdc  9307  fzodcel  10576  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  suprzubdc  10687  nninfdcex  10688  zsupssdc  10689  qdcle  10697  nn0sqdc  11167  hashfibclem  11303  fzowrddc  11440  sumeq1  12145  sumdc  12148  summodclem2  12173  summodc  12174  zsumdc  12175  fsum3  12178  isumz  12180  isumss  12182  fisumss  12183  isumss2  12184  fsum3cvg2  12185  fsumsersdc  12186  fsumsplit  12198  prodeq1f  12343  prodmodclem2a  12367  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodseq  12374  prod1dc  12377  prodssdc  12380  fprodssdc  12381  fprodsplitdc  12387  dvdsdc  12589  zdvdsdc  12603  bitsdc  12738  nnmindc  12835  nnminle  12836  uzwodc  12838  nnwosdc  12840  hashdvds  13027  eulerthlemfi  13034  dvdsfi  13045  phisum  13047  infpnlem2  13167  1arith  13174  4sqexercise1  13205  4sqexercise2  13206  4sqlemsdc  13207  ballotfilemcdc  13280  ballotfilemdifcfz  13284  ballotfilemefi  13294  ennnfonelemr  13371  ennnfonelemim  13372  ctinf  13378  ctiunctlemudc  13385  ctiunct  13388  ssomct  13393  ssnnctlemct  13394  nninfdclemcl  13396  nninfdclemp1  13398  gsumresfi  14262  psrbagfi  15166  psrbagdceq  15167  psrbaglecl  15172  psrbagcon  15174  psr1clfi  15207  ppiqub  16310  perfectlem2  16317  bpos  16337  lgsval  16345  lgsfvalg  16346  lgsfcl2  16347  lgsval2lem  16351  lgsdir2  16374  lgsne0  16379  2lgs  16445  2lgsoddprm  16454  vtxedgfi  16752  vtxlpfi  16753  eupth2lem3lem4fi  16936  sumdc2  17049  bj-charfundcALT  17057  bj-charfunbi  17059  pw1dceq  17257  nninfsellemdc  17276  iswomninnlem  17323  iswomni0  17325  redcwlpo  17329  redc0  17331  reap0  17332  cndcap  17333  dceqnconst  17334  dcapnconst  17335