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

Theorem dcbid 786
Description: The equivalent of a decidable proposition is decidable. (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 627 . . 3 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
31, 2orbi12d 742 . 2 (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4 df-dc 781 . 2 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5 df-dc 781 . 2 (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
63, 4, 53bitr4g 221 1 (𝜑 → (DECID 𝜓DECID 𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 103  wo 664  DECID wdc 780
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665
This theorem depends on definitions:  df-bi 115  df-dc 781
This theorem is referenced by:  exmidexmid  4031  exmidel  4034  dcdifsnid  6263  finexdc  6616  undifdcss  6631  ssfirab  6641  fidcenumlemrks  6660  ltdcpi  6880  enqdc  6918  enqdc1  6919  ltdcnq  6954  fzodcel  9559  exfzdc  9647  sumeq1  10740  sumdc  10743  isummolem2  10768  isummo  10769  zisum  10770  fisum  10774  isumz  10777  isumss  10779  fisumss  10780  isumss2  10781  fisumcvg2  10782  fsum3cvg2  10783  fisumsers  10784  fsumsplit  10797  dvdsdc  11078  zdvdsdc  11091  zsupcllemstep  11215  infssuzex  11219  hashdvds  11471  sumdc2  11654  nninfsellemdc  11857
  Copyright terms: Public domain W3C validator