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  4229  exmidel  4238  dcdifsnid  6562  pw2f1odclem  6895  finexdc  6963  pw1dc1  6975  undifdcss  6984  prfidceq  6989  tpfidceq  6991  ssfirab  6997  opabfi  6999  infidc  7000  fidcenumlemrks  7019  dcfi  7047  difinfsnlem  7165  difinfsn  7166  ctssdclemn0  7176  ctssdccl  7177  ctssdclemr  7178  ctssdc  7179  iswomni  7231  enwomnilem  7235  nninfdcinf  7237  nninfwlporlem  7239  nninfwlpoimlemdc  7243  nninfwlpoim  7244  netap  7321  ltdcpi  7390  enqdc  7428  enqdc1  7429  ltdcnq  7464  fzodcel  10228  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  suprzubdc  10326  nninfdcex  10327  zsupssdc  10328  qdcle  10336  sumeq1  11520  sumdc  11523  summodclem2  11547  summodc  11548  zsumdc  11549  fsum3  11552  isumz  11554  isumss  11556  fisumss  11557  isumss2  11558  fsum3cvg2  11559  fsumsersdc  11560  fsumsplit  11572  prodeq1f  11717  prodmodclem2a  11741  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodseq  11748  prod1dc  11751  prodssdc  11754  fprodssdc  11755  fprodsplitdc  11761  dvdsdc  11963  zdvdsdc  11977  nnmindc  12201  nnminle  12202  uzwodc  12204  nnwosdc  12206  hashdvds  12389  eulerthlemfi  12396  dvdsfi  12407  phisum  12409  infpnlem2  12529  1arith  12536  4sqexercise1  12567  4sqexercise2  12568  4sqlemsdc  12569  ennnfonelemr  12640  ennnfonelemim  12641  ctinf  12647  ctiunctlemudc  12654  ctiunct  12657  ssomct  12662  ssnnctlemct  12663  nninfdclemcl  12665  nninfdclemp1  12667  perfectlem2  15236  lgsval  15245  lgsfvalg  15246  lgsfcl2  15247  lgsval2lem  15251  lgsdir2  15274  lgsne0  15279  2lgs  15345  2lgsoddprm  15354  sumdc2  15445  bj-charfundcALT  15455  bj-charfunbi  15457  nninfsellemdc  15654  iswomninnlem  15693  iswomni0  15695  redcwlpo  15699  redc0  15701  reap0  15702  cndcap  15703  dceqnconst  15704  dcapnconst  15705