Theorem dcbid 846

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

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

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 619  ax-in2 620  ax-io 717

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

This theorem is referenced by:  dcbiit  847  exmidexmid  4292  exmidel  4301  suppssdc  6438  dcdifsnid  6715  pw2f1odclem  7063  finexdc  7135  elssdc  7137  eqsndc  7138  pw1dc1  7149  undifdcss  7158  prfidceq  7163  tpfidceq  7165  ssfirab  7172  opabfi  7175  infidc  7176  fidcenumlemrks  7195  dcfi  7223  difinfsnlem  7341  difinfsn  7342  ctssdclemn0  7352  ctssdccl  7353  ctssdclemr  7354  ctssdc  7355  iswomni  7407  enwomnilem  7411  nninfdcinf  7413  nninfwlporlem  7415  nninfwlpoimlemdc  7419  nninfinfwlpolem  7420  nninfwlpoim  7421  nninfinfwlpo  7422  netap  7516  ltdcpi  7586  enqdc  7624  enqdc1  7625  ltdcnq  7660  fzodcel  10433  exfzdc  10532  zsupcllemstep  10535  infssuzex  10539  suprzubdc  10542  nninfdcex  10543  zsupssdc  10544  qdcle  10552  fzowrddc  11277  sumeq1  11978  sumdc  11981  summodclem2  12006  summodc  12007  zsumdc  12008  fsum3  12011  isumz  12013  isumss  12015  fisumss  12016  isumss2  12017  fsum3cvg2  12018  fsumsersdc  12019  fsumsplit  12031  prodeq1f  12176  prodmodclem2a  12200  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodseq  12207  prod1dc  12210  prodssdc  12213  fprodssdc  12214  fprodsplitdc  12220  dvdsdc  12422  zdvdsdc  12436  bitsdc  12571  nnmindc  12668  nnminle  12669  uzwodc  12671  nnwosdc  12673  hashdvds  12856  eulerthlemfi  12863  dvdsfi  12874  phisum  12876  infpnlem2  12996  1arith  13003  4sqexercise1  13034  4sqexercise2  13035  4sqlemsdc  13036  ennnfonelemr  13107  ennnfonelemim  13108  ctinf  13114  ctiunctlemudc  13121  ctiunct  13124  ssomct  13129  ssnnctlemct  13130  nninfdclemcl  13132  nninfdclemp1  13134  psrbagfi  14753  psrbaglecl  14754  psrbagcon  14755  psr1clfi  14772  perfectlem2  15797  lgsval  15806  lgsfvalg  15807  lgsfcl2  15808  lgsval2lem  15812  lgsdir2  15835  lgsne0  15840  2lgs  15906  2lgsoddprm  15915  vtxedgfi  16213  vtxlpfi  16214  eupth2lem3lem4fi  16397  sumdc2  16500  bj-charfundcALT  16508  bj-charfunbi  16510  2omap  16698  pw1dceq  16709  nninfsellemdc  16719  iswomninnlem  16765  iswomni0  16767  redcwlpo  16771  redc0  16773  reap0  16774  cndcap  16775  dceqnconst  16776  dcapnconst  16777