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  6508  finexdc  6905  pw1dc1  6916  undifdcss  6925  ssfirab  6936  fidcenumlemrks  6955  dcfi  6983  difinfsnlem  7101  difinfsn  7102  ctssdclemn0  7112  ctssdccl  7113  ctssdclemr  7114  ctssdc  7115  iswomni  7166  enwomnilem  7170  nninfdcinf  7172  nninfwlporlem  7174  nninfwlpoimlemdc  7178  nninfwlpoim  7179  netap  7256  ltdcpi  7325  enqdc  7363  enqdc1  7364  ltdcnq  7399  fzodcel  10155  exfzdc  10243  sumeq1  11366  sumdc  11369  summodclem2  11393  summodc  11394  zsumdc  11395  fsum3  11398  isumz  11400  isumss  11402  fisumss  11403  isumss2  11404  fsum3cvg2  11405  fsumsersdc  11406  fsumsplit  11418  prodeq1f  11563  prodmodclem2a  11587  prodmodclem2  11588  prodmodc  11589  zproddc  11590  fprodseq  11594  prod1dc  11597  prodssdc  11600  fprodssdc  11601  fprodsplitdc  11607  dvdsdc  11808  zdvdsdc  11822  zsupcllemstep  11949  infssuzex  11953  suprzubdc  11956  nninfdcex  11957  zsupssdc  11958  nnmindc  12038  nnminle  12039  uzwodc  12041  nnwosdc  12043  hashdvds  12224  eulerthlemfi  12231  phisum  12243  infpnlem2  12361  1arith  12368  ennnfonelemr  12427  ennnfonelemim  12428  ctinf  12434  ctiunctlemudc  12441  ctiunct  12444  ssomct  12449  ssnnctlemct  12450  nninfdclemcl  12452  nninfdclemp1  12454  lgsval  14566  lgsfvalg  14567  lgsfcl2  14568  lgsval2lem  14572  lgsdir2  14595  lgsne0  14600  sumdc2  14712  bj-charfundcALT  14722  bj-charfunbi  14724  nninfsellemdc  14921  iswomninnlem  14959  iswomni0  14961  redcwlpo  14965  redc0  14967  reap0  14968  cndcap  14969  dceqnconst  14970  dcapnconst  14971