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  4230  exmidel  4239  dcdifsnid  6571  pw2f1odclem  6904  finexdc  6972  pw1dc1  6984  undifdcss  6993  prfidceq  6998  tpfidceq  7000  ssfirab  7006  opabfi  7008  infidc  7009  fidcenumlemrks  7028  dcfi  7056  difinfsnlem  7174  difinfsn  7175  ctssdclemn0  7185  ctssdccl  7186  ctssdclemr  7187  ctssdc  7188  iswomni  7240  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemdc  7252  nninfinfwlpolem  7253  nninfwlpoim  7254  nninfinfwlpo  7255  netap  7339  ltdcpi  7409  enqdc  7447  enqdc1  7448  ltdcnq  7483  fzodcel  10247  exfzdc  10335  zsupcllemstep  10338  infssuzex  10342  suprzubdc  10345  nninfdcex  10346  zsupssdc  10347  qdcle  10355  sumeq1  11539  sumdc  11542  summodclem2  11566  summodc  11567  zsumdc  11568  fsum3  11571  isumz  11573  isumss  11575  fisumss  11576  isumss2  11577  fsum3cvg2  11578  fsumsersdc  11579  fsumsplit  11591  prodeq1f  11736  prodmodclem2a  11760  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodseq  11767  prod1dc  11770  prodssdc  11773  fprodssdc  11774  fprodsplitdc  11780  dvdsdc  11982  zdvdsdc  11996  bitsdc  12131  nnmindc  12228  nnminle  12229  uzwodc  12231  nnwosdc  12233  hashdvds  12416  eulerthlemfi  12423  dvdsfi  12434  phisum  12436  infpnlem2  12556  1arith  12563  4sqexercise1  12594  4sqexercise2  12595  4sqlemsdc  12596  ennnfonelemr  12667  ennnfonelemim  12668  ctinf  12674  ctiunctlemudc  12681  ctiunct  12684  ssomct  12689  ssnnctlemct  12690  nninfdclemcl  12692  nninfdclemp1  12694  psrbagfi  14307  psr1clfi  14322  perfectlem2  15344  lgsval  15353  lgsfvalg  15354  lgsfcl2  15355  lgsval2lem  15359  lgsdir2  15382  lgsne0  15387  2lgs  15453  2lgsoddprm  15462  sumdc2  15553  bj-charfundcALT  15563  bj-charfunbi  15565  2omap  15750  nninfsellemdc  15765  iswomninnlem  15806  iswomni0  15808  redcwlpo  15812  redc0  15814  reap0  15815  cndcap  15816  dceqnconst  15817  dcapnconst  15818