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  4256  exmidel  4265  dcdifsnid  6613  pw2f1odclem  6956  finexdc  7025  pw1dc1  7037  undifdcss  7046  prfidceq  7051  tpfidceq  7053  ssfirab  7059  opabfi  7061  infidc  7062  fidcenumlemrks  7081  dcfi  7109  difinfsnlem  7227  difinfsn  7228  ctssdclemn0  7238  ctssdccl  7239  ctssdclemr  7240  ctssdc  7241  iswomni  7293  enwomnilem  7297  nninfdcinf  7299  nninfwlporlem  7301  nninfwlpoimlemdc  7305  nninfinfwlpolem  7306  nninfwlpoim  7307  nninfinfwlpo  7308  netap  7401  ltdcpi  7471  enqdc  7509  enqdc1  7510  ltdcnq  7545  fzodcel  10310  exfzdc  10406  zsupcllemstep  10409  infssuzex  10413  suprzubdc  10416  nninfdcex  10417  zsupssdc  10418  qdcle  10426  fzowrddc  11138  sumeq1  11781  sumdc  11784  summodclem2  11808  summodc  11809  zsumdc  11810  fsum3  11813  isumz  11815  isumss  11817  fisumss  11818  isumss2  11819  fsum3cvg2  11820  fsumsersdc  11821  fsumsplit  11833  prodeq1f  11978  prodmodclem2a  12002  prodmodclem2  12003  prodmodc  12004  zproddc  12005  fprodseq  12009  prod1dc  12012  prodssdc  12015  fprodssdc  12016  fprodsplitdc  12022  dvdsdc  12224  zdvdsdc  12238  bitsdc  12373  nnmindc  12470  nnminle  12471  uzwodc  12473  nnwosdc  12475  hashdvds  12658  eulerthlemfi  12665  dvdsfi  12676  phisum  12678  infpnlem2  12798  1arith  12805  4sqexercise1  12836  4sqexercise2  12837  4sqlemsdc  12838  ennnfonelemr  12909  ennnfonelemim  12910  ctinf  12916  ctiunctlemudc  12923  ctiunct  12926  ssomct  12931  ssnnctlemct  12932  nninfdclemcl  12934  nninfdclemp1  12936  psrbagfi  14550  psr1clfi  14565  perfectlem2  15587  lgsval  15596  lgsfvalg  15597  lgsfcl2  15598  lgsval2lem  15602  lgsdir2  15625  lgsne0  15630  2lgs  15696  2lgsoddprm  15705  sumdc2  15935  bj-charfundcALT  15944  bj-charfunbi  15946  2omap  16132  nninfsellemdc  16149  iswomninnlem  16190  iswomni0  16192  redcwlpo  16196  redc0  16198  reap0  16199  cndcap  16200  dceqnconst  16201  dcapnconst  16202