Theorem dcbid 839

Description: Equivalence property for decidability. Deduction form. (Contributed by Jim Kingdon, 7-Sep-2019.)

Hypothesis

Ref	Expression
dcbid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
dcbid	|- ( ph -> (DECID ps <-> DECID ch ) )

Proof of Theorem dcbid

Step	Hyp	Ref	Expression
1		dcbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	notbid 668	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 794	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 836	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 836	. 2 |- (DECID ch <-> ( ch \/ -. ch ) )
6	3, 4, 5	3bitr4g 223	1 |- ( ph -> (DECID ps <-> DECID ch ) )

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  4226  exmidel  4235  dcdifsnid  6559  pw2f1odclem  6892  finexdc  6960  pw1dc1  6972  undifdcss  6981  ssfirab  6992  opabfi  6994  infidc  6995  fidcenumlemrks  7014  dcfi  7042  difinfsnlem  7160  difinfsn  7161  ctssdclemn0  7171  ctssdccl  7172  ctssdclemr  7173  ctssdc  7174  iswomni  7226  enwomnilem  7230  nninfdcinf  7232  nninfwlporlem  7234  nninfwlpoimlemdc  7238  nninfwlpoim  7239  netap  7316  ltdcpi  7385  enqdc  7423  enqdc1  7424  ltdcnq  7459  fzodcel  10222  exfzdc  10310  sumeq1  11501  sumdc  11504  summodclem2  11528  summodc  11529  zsumdc  11530  fsum3  11533  isumz  11535  isumss  11537  fisumss  11538  isumss2  11539  fsum3cvg2  11540  fsumsersdc  11541  fsumsplit  11553  prodeq1f  11698  prodmodclem2a  11722  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodseq  11729  prod1dc  11732  prodssdc  11735  fprodssdc  11736  fprodsplitdc  11742  dvdsdc  11944  zdvdsdc  11958  zsupcllemstep  12085  infssuzex  12089  suprzubdc  12092  nninfdcex  12093  zsupssdc  12094  nnmindc  12174  nnminle  12175  uzwodc  12177  nnwosdc  12179  hashdvds  12362  eulerthlemfi  12369  phisum  12381  infpnlem2  12501  1arith  12508  4sqexercise1  12539  4sqexercise2  12540  4sqlemsdc  12541  ennnfonelemr  12583  ennnfonelemim  12584  ctinf  12590  ctiunctlemudc  12597  ctiunct  12600  ssomct  12605  ssnnctlemct  12606  nninfdclemcl  12608  nninfdclemp1  12610  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgsval2lem  15167  lgsdir2  15190  lgsne0  15195  2lgs  15261  2lgsoddprm  15270  sumdc2  15361  bj-charfundcALT  15371  bj-charfunbi  15373  nninfsellemdc  15570  iswomninnlem  15609  iswomni0  15611  redcwlpo  15615  redc0  15617  reap0  15618  cndcap  15619  dceqnconst  15620  dcapnconst  15621