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  4225  exmidel  4234  dcdifsnid  6557  pw2f1odclem  6890  finexdc  6958  pw1dc1  6970  undifdcss  6979  ssfirab  6990  opabfi  6992  infidc  6993  fidcenumlemrks  7012  dcfi  7040  difinfsnlem  7158  difinfsn  7159  ctssdclemn0  7169  ctssdccl  7170  ctssdclemr  7171  ctssdc  7172  iswomni  7224  enwomnilem  7228  nninfdcinf  7230  nninfwlporlem  7232  nninfwlpoimlemdc  7236  nninfwlpoim  7237  netap  7314  ltdcpi  7383  enqdc  7421  enqdc1  7422  ltdcnq  7457  fzodcel  10219  exfzdc  10307  sumeq1  11498  sumdc  11501  summodclem2  11525  summodc  11526  zsumdc  11527  fsum3  11530  isumz  11532  isumss  11534  fisumss  11535  isumss2  11536  fsum3cvg2  11537  fsumsersdc  11538  fsumsplit  11550  prodeq1f  11695  prodmodclem2a  11719  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodseq  11726  prod1dc  11729  prodssdc  11732  fprodssdc  11733  fprodsplitdc  11739  dvdsdc  11941  zdvdsdc  11955  zsupcllemstep  12082  infssuzex  12086  suprzubdc  12089  nninfdcex  12090  zsupssdc  12091  nnmindc  12171  nnminle  12172  uzwodc  12174  nnwosdc  12176  hashdvds  12359  eulerthlemfi  12366  phisum  12378  infpnlem2  12498  1arith  12505  4sqexercise1  12536  4sqexercise2  12537  4sqlemsdc  12538  ennnfonelemr  12580  ennnfonelemim  12581  ctinf  12587  ctiunctlemudc  12594  ctiunct  12597  ssomct  12602  ssnnctlemct  12603  nninfdclemcl  12605  nninfdclemp1  12607  lgsval  15120  lgsfvalg  15121  lgsfcl2  15122  lgsval2lem  15126  lgsdir2  15149  lgsne0  15154  sumdc2  15291  bj-charfundcALT  15301  bj-charfunbi  15303  nninfsellemdc  15500  iswomninnlem  15539  iswomni0  15541  redcwlpo  15545  redc0  15547  reap0  15548  cndcap  15549  dceqnconst  15550  dcapnconst  15551