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

Theorem dcbid 833
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 662 . . 3 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
31, 2orbi12d 788 . 2 (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4 df-dc 830 . 2 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5 df-dc 830 . 2 (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
63, 4, 53bitr4g 222 1 (𝜑 → (DECID 𝜓DECID 𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 104  wo 703  DECID wdc 829
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 609  ax-in2 610  ax-io 704
This theorem depends on definitions:  df-bi 116  df-dc 830
This theorem is referenced by:  dcbiit  834  exmidexmid  4182  exmidel  4191  dcdifsnid  6483  finexdc  6880  pw1dc1  6891  undifdcss  6900  ssfirab  6911  fidcenumlemrks  6930  dcfi  6958  difinfsnlem  7076  difinfsn  7077  ctssdclemn0  7087  ctssdccl  7088  ctssdclemr  7089  ctssdc  7090  iswomni  7141  enwomnilem  7145  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemdc  7153  nninfwlpoim  7154  ltdcpi  7285  enqdc  7323  enqdc1  7324  ltdcnq  7359  fzodcel  10108  exfzdc  10196  sumeq1  11318  sumdc  11321  summodclem2  11345  summodc  11346  zsumdc  11347  fsum3  11350  isumz  11352  isumss  11354  fisumss  11355  isumss2  11356  fsum3cvg2  11357  fsumsersdc  11358  fsumsplit  11370  prodeq1f  11515  prodmodclem2a  11539  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodseq  11546  prod1dc  11549  prodssdc  11552  fprodssdc  11553  fprodsplitdc  11559  dvdsdc  11760  zdvdsdc  11774  zsupcllemstep  11900  infssuzex  11904  suprzubdc  11907  nninfdcex  11908  zsupssdc  11909  nnmindc  11989  nnminle  11990  uzwodc  11992  nnwosdc  11994  hashdvds  12175  eulerthlemfi  12182  phisum  12194  infpnlem2  12312  1arith  12319  ennnfonelemr  12378  ennnfonelemim  12379  ctinf  12385  ctiunctlemudc  12392  ctiunct  12395  ssomct  12400  ssnnctlemct  12401  nninfdclemcl  12403  nninfdclemp1  12405  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgsval2lem  13705  lgsdir2  13728  lgsne0  13733  sumdc2  13834  bj-charfundcALT  13844  bj-charfunbi  13846  nninfsellemdc  14043  iswomninnlem  14081  iswomni0  14083  redcwlpo  14087  redc0  14089  reap0  14090  dceqnconst  14091  dcapnconst  14092
  Copyright terms: Public domain W3C validator