Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  dcbid Unicode version

Theorem dcbid 823
 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
StepHypRef Expression
1 dcbid.1 . . 3
21notbid 656 . . 3
31, 2orbi12d 782 . 2
4 df-dc 820 . 2 DECID
5 df-dc 820 . 2 DECID
63, 4, 53bitr4g 222 1 DECID DECID
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 104   wo 697  DECID wdc 819 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 603  ax-in2 604  ax-io 698 This theorem depends on definitions:  df-bi 116  df-dc 820 This theorem is referenced by:  dcbiit  824  exmidexmid  4120  exmidel  4128  dcdifsnid  6400  finexdc  6796  undifdcss  6811  ssfirab  6822  fidcenumlemrks  6841  difinfsnlem  6984  difinfsn  6985  ctssdclemn0  6995  ctssdccl  6996  ctssdclemr  6997  ctssdc  6998  ltdcpi  7131  enqdc  7169  enqdc1  7170  ltdcnq  7205  fzodcel  9929  exfzdc  10017  sumeq1  11124  sumdc  11127  summodclem2  11151  summodc  11152  zsumdc  11153  fsum3  11156  isumz  11158  isumss  11160  fisumss  11161  isumss2  11162  fsum3cvg2  11163  fsumsersdc  11164  fsumsplit  11176  prodeq1f  11321  prodmodclem2a  11345  prodmodclem2  11346  prodmodc  11347  dvdsdc  11501  zdvdsdc  11514  zsupcllemstep  11638  infssuzex  11642  hashdvds  11897  ennnfonelemr  11936  ennnfonelemim  11937  ctinf  11943  ctiunctlemudc  11950  ctiunct  11953  sumdc2  13006  nninfsellemdc  13206
 Copyright terms: Public domain W3C validator