Theorem dcbid 838

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 667	. . 3 |- ( ph -> ( -. ps <-> -. ch ) )
3	1, 2	orbi12d 793	. 2 |- ( ph -> ( ( ps \/ -. ps ) <-> ( ch \/ -. ch ) ) )
4		df-dc 835	. 2 |- (DECID ps <-> ( ps \/ -. ps ) )
5		df-dc 835	. 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 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  6507  finexdc  6904  pw1dc1  6915  undifdcss  6924  ssfirab  6935  fidcenumlemrks  6954  dcfi  6982  difinfsnlem  7100  difinfsn  7101  ctssdclemn0  7111  ctssdccl  7112  ctssdclemr  7113  ctssdc  7114  iswomni  7165  enwomnilem  7169  nninfdcinf  7171  nninfwlporlem  7173  nninfwlpoimlemdc  7177  nninfwlpoim  7178  netap  7255  ltdcpi  7324  enqdc  7362  enqdc1  7363  ltdcnq  7398  fzodcel  10154  exfzdc  10242  sumeq1  11365  sumdc  11368  summodclem2  11392  summodc  11393  zsumdc  11394  fsum3  11397  isumz  11399  isumss  11401  fisumss  11402  isumss2  11403  fsum3cvg2  11404  fsumsersdc  11405  fsumsplit  11417  prodeq1f  11562  prodmodclem2a  11586  prodmodclem2  11587  prodmodc  11588  zproddc  11589  fprodseq  11593  prod1dc  11596  prodssdc  11599  fprodssdc  11600  fprodsplitdc  11606  dvdsdc  11807  zdvdsdc  11821  zsupcllemstep  11948  infssuzex  11952  suprzubdc  11955  nninfdcex  11956  zsupssdc  11957  nnmindc  12037  nnminle  12038  uzwodc  12040  nnwosdc  12042  hashdvds  12223  eulerthlemfi  12230  phisum  12242  infpnlem2  12360  1arith  12367  ennnfonelemr  12426  ennnfonelemim  12427  ctinf  12433  ctiunctlemudc  12440  ctiunct  12443  ssomct  12448  ssnnctlemct  12449  nninfdclemcl  12451  nninfdclemp1  12453  lgsval  14444  lgsfvalg  14445  lgsfcl2  14446  lgsval2lem  14450  lgsdir2  14473  lgsne0  14478  sumdc2  14590  bj-charfundcALT  14600  bj-charfunbi  14602  nninfsellemdc  14798  iswomninnlem  14836  iswomni0  14838  redcwlpo  14842  redc0  14844  reap0  14845  cndcap  14846  dceqnconst  14847  dcapnconst  14848