Theorem dcbid 843

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

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

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 617  ax-in2 618  ax-io 714

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

This theorem is referenced by:  dcbiit  844  exmidexmid  4280  exmidel  4289  dcdifsnid  6658  pw2f1odclem  7003  finexdc  7073  elssdc  7075  eqsndc  7076  pw1dc1  7087  undifdcss  7096  prfidceq  7101  tpfidceq  7103  ssfirab  7109  opabfi  7111  infidc  7112  fidcenumlemrks  7131  dcfi  7159  difinfsnlem  7277  difinfsn  7278  ctssdclemn0  7288  ctssdccl  7289  ctssdclemr  7290  ctssdc  7291  iswomni  7343  enwomnilem  7347  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemdc  7355  nninfinfwlpolem  7356  nninfwlpoim  7357  nninfinfwlpo  7358  netap  7451  ltdcpi  7521  enqdc  7559  enqdc1  7560  ltdcnq  7595  fzodcel  10361  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  nninfdcex  10469  zsupssdc  10470  qdcle  10478  fzowrddc  11195  sumeq1  11882  sumdc  11885  summodclem2  11909  summodc  11910  zsumdc  11911  fsum3  11914  isumz  11916  isumss  11918  fisumss  11919  isumss2  11920  fsum3cvg2  11921  fsumsersdc  11922  fsumsplit  11934  prodeq1f  12079  prodmodclem2a  12103  prodmodclem2  12104  prodmodc  12105  zproddc  12106  fprodseq  12110  prod1dc  12113  prodssdc  12116  fprodssdc  12117  fprodsplitdc  12123  dvdsdc  12325  zdvdsdc  12339  bitsdc  12474  nnmindc  12571  nnminle  12572  uzwodc  12574  nnwosdc  12576  hashdvds  12759  eulerthlemfi  12766  dvdsfi  12777  phisum  12779  infpnlem2  12899  1arith  12906  4sqexercise1  12937  4sqexercise2  12938  4sqlemsdc  12939  ennnfonelemr  13010  ennnfonelemim  13011  ctinf  13017  ctiunctlemudc  13024  ctiunct  13027  ssomct  13032  ssnnctlemct  13033  nninfdclemcl  13035  nninfdclemp1  13037  psrbagfi  14653  psr1clfi  14668  perfectlem2  15690  lgsval  15699  lgsfvalg  15700  lgsfcl2  15701  lgsval2lem  15705  lgsdir2  15728  lgsne0  15733  2lgs  15799  2lgsoddprm  15808  vtxedgfi  16049  vtxlpfi  16050  sumdc2  16246  bj-charfundcALT  16255  bj-charfunbi  16257  2omap  16446  pw1dceq  16457  nninfsellemdc  16464  iswomninnlem  16505  iswomni0  16507  redcwlpo  16511  redc0  16513  reap0  16514  cndcap  16515  dceqnconst  16516  dcapnconst  16517