Theorem dcbid 824

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 657	. . 3 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
3	1, 2	orbi12d 783	. 2 ⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4		df-dc 821	. 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5		df-dc 821	. 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
6	3, 4, 5	3bitr4g 222	1 ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   ∨ wo 698  DECID wdc 820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116  df-dc 821

This theorem is referenced by:  dcbiit  825  exmidexmid  4158  exmidel  4167  dcdifsnid  6452  finexdc  6848  pw1dc1  6859  undifdcss  6868  ssfirab  6879  fidcenumlemrks  6898  dcfi  6926  difinfsnlem  7044  difinfsn  7045  ctssdclemn0  7055  ctssdccl  7056  ctssdclemr  7057  ctssdc  7058  iswomni  7109  enwomnilem  7113  ltdcpi  7244  enqdc  7282  enqdc1  7283  ltdcnq  7318  fzodcel  10055  exfzdc  10143  sumeq1  11256  sumdc  11259  summodclem2  11283  summodc  11284  zsumdc  11285  fsum3  11288  isumz  11290  isumss  11292  fisumss  11293  isumss2  11294  fsum3cvg2  11295  fsumsersdc  11296  fsumsplit  11308  prodeq1f  11453  prodmodclem2a  11477  prodmodclem2  11478  prodmodc  11479  zproddc  11480  fprodseq  11484  prod1dc  11487  prodssdc  11490  fprodssdc  11491  fprodsplitdc  11497  dvdsdc  11698  zdvdsdc  11712  zsupcllemstep  11836  infssuzex  11840  nninfdcex  11843  hashdvds  12100  eulerthlemfi  12107  phisum  12119  ennnfonelemr  12194  ennnfonelemim  12195  ctinf  12201  ctiunctlemudc  12208  ctiunct  12211  ssomct  12216  ssnnctlemct  12217  nnmindc  12219  nnminle  12220  nninfdclemcl  12221  nninfdclemp1  12223  sumdc2  13415  bj-charfundcALT  13426  bj-charfunbi  13428  nninfsellemdc  13624  iswomninnlem  13662  iswomni0  13664  redcwlpo  13668  redc0  13670  reap0  13671  dceqnconst  13672  dcapnconst  13673