Theorem dcbid 843

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

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

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 617  ax-in2 618  ax-io 714

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

This theorem is referenced by:  dcbiit  844  exmidexmid  4280  exmidel  4289  dcdifsnid  6650  pw2f1odclem  6995  finexdc  7064  pw1dc1  7076  undifdcss  7085  prfidceq  7090  tpfidceq  7092  ssfirab  7098  opabfi  7100  infidc  7101  fidcenumlemrks  7120  dcfi  7148  difinfsnlem  7266  difinfsn  7267  ctssdclemn0  7277  ctssdccl  7278  ctssdclemr  7279  ctssdc  7280  iswomni  7332  enwomnilem  7336  nninfdcinf  7338  nninfwlporlem  7340  nninfwlpoimlemdc  7344  nninfinfwlpolem  7345  nninfwlpoim  7346  nninfinfwlpo  7347  netap  7440  ltdcpi  7510  enqdc  7548  enqdc1  7549  ltdcnq  7584  fzodcel  10349  exfzdc  10446  zsupcllemstep  10449  infssuzex  10453  suprzubdc  10456  nninfdcex  10457  zsupssdc  10458  qdcle  10466  fzowrddc  11179  sumeq1  11866  sumdc  11869  summodclem2  11893  summodc  11894  zsumdc  11895  fsum3  11898  isumz  11900  isumss  11902  fisumss  11903  isumss2  11904  fsum3cvg2  11905  fsumsersdc  11906  fsumsplit  11918  prodeq1f  12063  prodmodclem2a  12087  prodmodclem2  12088  prodmodc  12089  zproddc  12090  fprodseq  12094  prod1dc  12097  prodssdc  12100  fprodssdc  12101  fprodsplitdc  12107  dvdsdc  12309  zdvdsdc  12323  bitsdc  12458  nnmindc  12555  nnminle  12556  uzwodc  12558  nnwosdc  12560  hashdvds  12743  eulerthlemfi  12750  dvdsfi  12761  phisum  12763  infpnlem2  12883  1arith  12890  4sqexercise1  12921  4sqexercise2  12922  4sqlemsdc  12923  ennnfonelemr  12994  ennnfonelemim  12995  ctinf  13001  ctiunctlemudc  13008  ctiunct  13011  ssomct  13016  ssnnctlemct  13017  nninfdclemcl  13019  nninfdclemp1  13021  psrbagfi  14637  psr1clfi  14652  perfectlem2  15674  lgsval  15683  lgsfvalg  15684  lgsfcl2  15685  lgsval2lem  15689  lgsdir2  15712  lgsne0  15717  2lgs  15783  2lgsoddprm  15792  sumdc2  16163  bj-charfundcALT  16172  bj-charfunbi  16174  2omap  16359  nninfsellemdc  16376  iswomninnlem  16417  iswomni0  16419  redcwlpo  16423  redc0  16425  reap0  16426  cndcap  16427  dceqnconst  16428  dcapnconst  16429