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  dcdifsnid  6781  pw2f1odclem  7138  finexdc  7211  elssdc  7213  eqsndc  7214  pw1dc1  7225  undifdcss  7234  prfidceq  7239  tpfidceq  7241  ssfirab  7248  opabfi  7251  infidc  7252  fissfi  7267  relresfin  7268  fidcenumlemrks  7275  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  10577  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  nninfdcex  10689  zsupssdc  10690  qdcle  10698  nn0sqdc  11168  hashfibclem  11304  fzowrddc  11441  sumeq1  12146  sumdc  12149  summodclem2  12174  summodc  12175  zsumdc  12176  fsum3  12179  isumz  12181  isumss  12183  fisumss  12184  isumss2  12185  fsum3cvg2  12186  fsumsersdc  12187  fsumsplit  12199  prodeq1f  12344  prodmodclem2a  12368  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodseq  12375  prod1dc  12378  prodssdc  12381  fprodssdc  12382  fprodsplitdc  12388  dvdsdc  12590  zdvdsdc  12604  bitsdc  12739  nnmindc  12836  nnminle  12837  uzwodc  12839  nnwosdc  12841  hashdvds  13028  eulerthlemfi  13035  dvdsfi  13046  phisum  13048  infpnlem2  13168  1arith  13175  4sqexercise1  13206  4sqexercise2  13207  4sqlemsdc  13208  ballotfilemcdc  13281  ballotfilemdifcfz  13285  ballotfilemefi  13295  ennnfonelemr  13372  ennnfonelemim  13373  ctinf  13379  ctiunctlemudc  13386  ctiunct  13389  ssomct  13394  ssnnctlemct  13395  nninfdclemcl  13397  nninfdclemp1  13399  gsumresfi  14263  psrbagfi  15168  psrbaglecl  15169  psrbagcon  15171  psr1clfi  15198  ppiqub  16293  perfectlem2  16300  bpos  16320  lgsval  16328  lgsfvalg  16329  lgsfcl2  16330  lgsval2lem  16334  lgsdir2  16357  lgsne0  16362  2lgs  16428  2lgsoddprm  16437  vtxedgfi  16735  vtxlpfi  16736  eupth2lem3lem4fi  16919  sumdc2  17032  bj-charfundcALT  17040  bj-charfunbi  17042  pw1dceq  17240  nninfsellemdc  17259  iswomninnlem  17306  iswomni0  17308  redcwlpo  17312  redc0  17314  reap0  17315  cndcap  17316  dceqnconst  17317  dcapnconst  17318