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  2omap  7318  difinfsnlem  7439  difinfsn  7440  ctssdclemn0  7450  ctssdccl  7451  ctssdclemr  7452  ctssdc  7453  iswomni  7505  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemdc  7517  nninfinfwlpolem  7518  nninfwlpoim  7519  nninfinfwlpo  7520  netap  7620  ltdcpi  7690  enqdc  7728  enqdc1  7729  ltdcnq  7764  indfdc  9298  fzodcel  10560  exfzdc  10659  zsupcllemstep  10662  infssuzex  10666  suprzubdc  10671  nninfdcex  10672  zsupssdc  10673  qdcle  10681  hashfibclem  11282  fzowrddc  11419  sumeq1  12121  sumdc  12124  summodclem2  12149  summodc  12150  zsumdc  12151  fsum3  12154  isumz  12156  isumss  12158  fisumss  12159  isumss2  12160  fsum3cvg2  12161  fsumsersdc  12162  fsumsplit  12174  prodeq1f  12319  prodmodclem2a  12343  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodseq  12350  prod1dc  12353  prodssdc  12356  fprodssdc  12357  fprodsplitdc  12363  dvdsdc  12565  zdvdsdc  12579  bitsdc  12714  nnmindc  12811  nnminle  12812  uzwodc  12814  nnwosdc  12816  hashdvds  12999  eulerthlemfi  13006  dvdsfi  13017  phisum  13019  infpnlem2  13139  1arith  13146  4sqexercise1  13177  4sqexercise2  13178  4sqlemsdc  13179  ballotfilemcdc  13223  ballotfilemdifcfz  13227  ballotfilemefi  13237  ennnfonelemr  13314  ennnfonelemim  13315  ctinf  13321  ctiunctlemudc  13328  ctiunct  13331  ssomct  13336  ssnnctlemct  13337  nninfdclemcl  13339  nninfdclemp1  13341  psrbagfi  15059  psrbaglecl  15060  psrbagcon  15062  psr1clfi  15079  perfectlem2  16114  lgsval  16123  lgsfvalg  16124  lgsfcl2  16125  lgsval2lem  16129  lgsdir2  16152  lgsne0  16157  2lgs  16223  2lgsoddprm  16232  vtxedgfi  16530  vtxlpfi  16531  eupth2lem3lem4fi  16714  sumdc2  16827  bj-charfundcALT  16835  bj-charfunbi  16837  pw1dceq  17035  nninfsellemdc  17053  iswomninnlem  17099  iswomni0  17101  redcwlpo  17105  redc0  17107  reap0  17108  cndcap  17109  dceqnconst  17110  dcapnconst  17111