Theorem dcbid 828

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

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

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 825

This theorem is referenced by:  dcbiit  829  exmidexmid  4174  exmidel  4183  dcdifsnid  6468  finexdc  6864  pw1dc1  6875  undifdcss  6884  ssfirab  6895  fidcenumlemrks  6914  dcfi  6942  difinfsnlem  7060  difinfsn  7061  ctssdclemn0  7071  ctssdccl  7072  ctssdclemr  7073  ctssdc  7074  iswomni  7125  enwomnilem  7129  ltdcpi  7260  enqdc  7298  enqdc1  7299  ltdcnq  7334  fzodcel  10083  exfzdc  10171  sumeq1  11292  sumdc  11295  summodclem2  11319  summodc  11320  zsumdc  11321  fsum3  11324  isumz  11326  isumss  11328  fisumss  11329  isumss2  11330  fsum3cvg2  11331  fsumsersdc  11332  fsumsplit  11344  prodeq1f  11489  prodmodclem2a  11513  prodmodclem2  11514  prodmodc  11515  zproddc  11516  fprodseq  11520  prod1dc  11523  prodssdc  11526  fprodssdc  11527  fprodsplitdc  11533  dvdsdc  11734  zdvdsdc  11748  zsupcllemstep  11874  infssuzex  11878  suprzubdc  11881  nninfdcex  11882  zsupssdc  11883  nnmindc  11963  nnminle  11964  uzwodc  11966  nnwosdc  11968  hashdvds  12149  eulerthlemfi  12156  phisum  12168  infpnlem2  12286  1arith  12293  ennnfonelemr  12352  ennnfonelemim  12353  ctinf  12359  ctiunctlemudc  12366  ctiunct  12369  ssomct  12374  ssnnctlemct  12375  nninfdclemcl  12377  nninfdclemp1  12379  lgsval  13505  lgsfvalg  13506  lgsfcl2  13507  lgsval2lem  13511  lgsdir2  13534  lgsne0  13539  sumdc2  13640  bj-charfundcALT  13651  bj-charfunbi  13653  nninfsellemdc  13850  iswomninnlem  13888  iswomni0  13890  redcwlpo  13894  redc0  13896  reap0  13897  dceqnconst  13898  dcapnconst  13899