Theorem dcbid 838

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

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

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 614  ax-in2 615  ax-io 709

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

This theorem is referenced by:  dcbiit  839  exmidexmid  4198  exmidel  4207  dcdifsnid  6508  finexdc  6905  pw1dc1  6916  undifdcss  6925  ssfirab  6936  fidcenumlemrks  6955  dcfi  6983  difinfsnlem  7101  difinfsn  7102  ctssdclemn0  7112  ctssdccl  7113  ctssdclemr  7114  ctssdc  7115  iswomni  7166  enwomnilem  7170  nninfdcinf  7172  nninfwlporlem  7174  nninfwlpoimlemdc  7178  nninfwlpoim  7179  netap  7256  ltdcpi  7325  enqdc  7363  enqdc1  7364  ltdcnq  7399  fzodcel  10155  exfzdc  10243  sumeq1  11366  sumdc  11369  summodclem2  11393  summodc  11394  zsumdc  11395  fsum3  11398  isumz  11400  isumss  11402  fisumss  11403  isumss2  11404  fsum3cvg2  11405  fsumsersdc  11406  fsumsplit  11418  prodeq1f  11563  prodmodclem2a  11587  prodmodclem2  11588  prodmodc  11589  zproddc  11590  fprodseq  11594  prod1dc  11597  prodssdc  11600  fprodssdc  11601  fprodsplitdc  11607  dvdsdc  11808  zdvdsdc  11822  zsupcllemstep  11949  infssuzex  11953  suprzubdc  11956  nninfdcex  11957  zsupssdc  11958  nnmindc  12038  nnminle  12039  uzwodc  12041  nnwosdc  12043  hashdvds  12224  eulerthlemfi  12231  phisum  12243  infpnlem2  12361  1arith  12368  ennnfonelemr  12427  ennnfonelemim  12428  ctinf  12434  ctiunctlemudc  12441  ctiunct  12444  ssomct  12449  ssnnctlemct  12450  nninfdclemcl  12452  nninfdclemp1  12454  lgsval  14593  lgsfvalg  14594  lgsfcl2  14595  lgsval2lem  14599  lgsdir2  14622  lgsne0  14627  sumdc2  14739  bj-charfundcALT  14749  bj-charfunbi  14751  nninfsellemdc  14948  iswomninnlem  14986  iswomni0  14988  redcwlpo  14992  redc0  14994  reap0  14995  cndcap  14996  dceqnconst  14997  dcapnconst  14998