Theorem dcbid 850

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 720  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117  df-dc 847

This theorem is used by:  dcbiit  851  ifeqeqxdc  3687  exmidexmid  4333  exmidel  4342  suppssdc  6500  dcdifsnid  6777  pw2f1odclem  7134  finexdc  7207  elssdc  7209  eqsndc  7210  pw1dc1  7221  undifdcss  7230  prfidceq  7235  tpfidceq  7237  ssfirab  7244  opabfi  7247  infidc  7248  fissfi  7263  fidcenumlemrks  7270  dcfi  7315  ofrfidc  7318  2omap  7319  difinfsnlem  7440  difinfsn  7441  ctssdclemn0  7451  ctssdccl  7452  ctssdclemr  7453  ctssdc  7454  iswomni  7506  enwomnilem  7510  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemdc  7518  nninfinfwlpolem  7519  nninfwlpoim  7520  nninfinfwlpo  7521  netap  7621  ltdcpi  7691  enqdc  7729  enqdc1  7730  ltdcnq  7765  indfdc  9301  fzodcel  10571  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  suprzubdc  10682  nninfdcex  10683  zsupssdc  10684  qdcle  10692  nn0sqdc  11162  hashfibclem  11298  fzowrddc  11435  sumeq1  12140  sumdc  12143  summodclem2  12168  summodc  12169  zsumdc  12170  fsum3  12173  isumz  12175  isumss  12177  fisumss  12178  isumss2  12179  fsum3cvg2  12180  fsumsersdc  12181  fsumsplit  12193  prodeq1f  12338  prodmodclem2a  12362  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodseq  12369  prod1dc  12372  prodssdc  12375  fprodssdc  12376  fprodsplitdc  12382  dvdsdc  12584  zdvdsdc  12598  bitsdc  12733  nnmindc  12830  nnminle  12831  uzwodc  12833  nnwosdc  12835  hashdvds  13022  eulerthlemfi  13029  dvdsfi  13040  phisum  13042  infpnlem2  13162  1arith  13169  4sqexercise1  13200  4sqexercise2  13201  4sqlemsdc  13202  ballotfilemcdc  13275  ballotfilemdifcfz  13279  ballotfilemefi  13289  ennnfonelemr  13366  ennnfonelemim  13367  ctinf  13373  ctiunctlemudc  13380  ctiunct  13383  ssomct  13388  ssnnctlemct  13389  nninfdclemcl  13391  nninfdclemp1  13393  psrbagfi  15143  psrbaglecl  15144  psrbagcon  15146  psr1clfi  15170  ppiqub  16254  perfectlem2  16261  bpos  16281  lgsval  16289  lgsfvalg  16290  lgsfcl2  16291  lgsval2lem  16295  lgsdir2  16318  lgsne0  16323  2lgs  16389  2lgsoddprm  16398  vtxedgfi  16696  vtxlpfi  16697  eupth2lem3lem4fi  16880  sumdc2  16993  bj-charfundcALT  17001  bj-charfunbi  17003  pw1dceq  17201  nninfsellemdc  17219  iswomninnlem  17266  iswomni0  17268  redcwlpo  17272  redc0  17274  reap0  17275  cndcap  17276  dceqnconst  17277  dcapnconst  17278