Theorem dcbid 839

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

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

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 710

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

This theorem is referenced by:  dcbiit  840  exmidexmid  4239  exmidel  4248  dcdifsnid  6589  pw2f1odclem  6930  finexdc  6998  pw1dc1  7010  undifdcss  7019  prfidceq  7024  tpfidceq  7026  ssfirab  7032  opabfi  7034  infidc  7035  fidcenumlemrks  7054  dcfi  7082  difinfsnlem  7200  difinfsn  7201  ctssdclemn0  7211  ctssdccl  7212  ctssdclemr  7213  ctssdc  7214  iswomni  7266  enwomnilem  7270  nninfdcinf  7272  nninfwlporlem  7274  nninfwlpoimlemdc  7278  nninfinfwlpolem  7279  nninfwlpoim  7280  nninfinfwlpo  7281  netap  7365  ltdcpi  7435  enqdc  7473  enqdc1  7474  ltdcnq  7509  fzodcel  10274  exfzdc  10367  zsupcllemstep  10370  infssuzex  10374  suprzubdc  10377  nninfdcex  10378  zsupssdc  10379  qdcle  10387  sumeq1  11637  sumdc  11640  summodclem2  11664  summodc  11665  zsumdc  11666  fsum3  11669  isumz  11671  isumss  11673  fisumss  11674  isumss2  11675  fsum3cvg2  11676  fsumsersdc  11677  fsumsplit  11689  prodeq1f  11834  prodmodclem2a  11858  prodmodclem2  11859  prodmodc  11860  zproddc  11861  fprodseq  11865  prod1dc  11868  prodssdc  11871  fprodssdc  11872  fprodsplitdc  11878  dvdsdc  12080  zdvdsdc  12094  bitsdc  12229  nnmindc  12326  nnminle  12327  uzwodc  12329  nnwosdc  12331  hashdvds  12514  eulerthlemfi  12521  dvdsfi  12532  phisum  12534  infpnlem2  12654  1arith  12661  4sqexercise1  12692  4sqexercise2  12693  4sqlemsdc  12694  ennnfonelemr  12765  ennnfonelemim  12766  ctinf  12772  ctiunctlemudc  12779  ctiunct  12782  ssomct  12787  ssnnctlemct  12788  nninfdclemcl  12790  nninfdclemp1  12792  psrbagfi  14406  psr1clfi  14421  perfectlem2  15443  lgsval  15452  lgsfvalg  15453  lgsfcl2  15454  lgsval2lem  15458  lgsdir2  15481  lgsne0  15486  2lgs  15552  2lgsoddprm  15561  sumdc2  15697  bj-charfundcALT  15707  bj-charfunbi  15709  2omap  15894  nninfsellemdc  15909  iswomninnlem  15950  iswomni0  15952  redcwlpo  15956  redc0  15958  reap0  15959  cndcap  15960  dceqnconst  15961  dcapnconst  15962