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

Theorem dcbid 782
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 625 . . 3 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
31, 2orbi12d 740 . 2 (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4 df-dc 777 . 2 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5 df-dc 777 . 2 (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
63, 4, 53bitr4g 221 1 (𝜑 → (DECID 𝜓DECID 𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 103  wo 662  DECID wdc 776
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 577  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115  df-dc 777
This theorem is referenced by:  exmidexmid  3995  exmidel  3998  dcdifsnid  6195  finexdc  6545  undifdcss  6560  ssfirab  6568  ltdcpi  6785  enqdc  6823  enqdc1  6824  ltdcnq  6859  exfzdc  9540  sumeq1  10566  sumdc  10569  dvdsdc  10584  zdvdsdc  10597  zsupcllemstep  10721  infssuzex  10725  hashdvds  10977  sumdc2  11042
  Copyright terms: Public domain W3C validator