Theorem dcbid 840

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

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

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 615  ax-in2 616  ax-io 711

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

This theorem is referenced by:  dcbiit  841  exmidexmid  4240  exmidel  4249  dcdifsnid  6590  pw2f1odclem  6931  finexdc  6999  pw1dc1  7011  undifdcss  7020  prfidceq  7025  tpfidceq  7027  ssfirab  7033  opabfi  7035  infidc  7036  fidcenumlemrks  7055  dcfi  7083  difinfsnlem  7201  difinfsn  7202  ctssdclemn0  7212  ctssdccl  7213  ctssdclemr  7214  ctssdc  7215  iswomni  7267  enwomnilem  7271  nninfdcinf  7273  nninfwlporlem  7275  nninfwlpoimlemdc  7279  nninfinfwlpolem  7280  nninfwlpoim  7281  nninfinfwlpo  7282  netap  7366  ltdcpi  7436  enqdc  7474  enqdc1  7475  ltdcnq  7510  fzodcel  10275  exfzdc  10369  zsupcllemstep  10372  infssuzex  10376  suprzubdc  10379  nninfdcex  10380  zsupssdc  10381  qdcle  10389  fzowrddc  11100  sumeq1  11666  sumdc  11669  summodclem2  11693  summodc  11694  zsumdc  11695  fsum3  11698  isumz  11700  isumss  11702  fisumss  11703  isumss2  11704  fsum3cvg2  11705  fsumsersdc  11706  fsumsplit  11718  prodeq1f  11863  prodmodclem2a  11887  prodmodclem2  11888  prodmodc  11889  zproddc  11890  fprodseq  11894  prod1dc  11897  prodssdc  11900  fprodssdc  11901  fprodsplitdc  11907  dvdsdc  12109  zdvdsdc  12123  bitsdc  12258  nnmindc  12355  nnminle  12356  uzwodc  12358  nnwosdc  12360  hashdvds  12543  eulerthlemfi  12550  dvdsfi  12561  phisum  12563  infpnlem2  12683  1arith  12690  4sqexercise1  12721  4sqexercise2  12722  4sqlemsdc  12723  ennnfonelemr  12794  ennnfonelemim  12795  ctinf  12801  ctiunctlemudc  12808  ctiunct  12811  ssomct  12816  ssnnctlemct  12817  nninfdclemcl  12819  nninfdclemp1  12821  psrbagfi  14435  psr1clfi  14450  perfectlem2  15472  lgsval  15481  lgsfvalg  15482  lgsfcl2  15483  lgsval2lem  15487  lgsdir2  15510  lgsne0  15515  2lgs  15581  2lgsoddprm  15590  sumdc2  15735  bj-charfundcALT  15745  bj-charfunbi  15747  2omap  15932  nninfsellemdc  15947  iswomninnlem  15988  iswomni0  15990  redcwlpo  15994  redc0  15996  reap0  15997  cndcap  15998  dceqnconst  15999  dcapnconst  16000