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

Theorem dcn 782
Description: A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.)
Assertion
Ref Expression
dcn (DECID 𝜑DECID ¬ 𝜑)

Proof of Theorem dcn
StepHypRef Expression
1 notnot 592 . . . 4 (𝜑 → ¬ ¬ 𝜑)
21orim2i 711 . . 3 ((¬ 𝜑𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
32orcoms 682 . 2 ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4 df-dc 779 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5 df-dc 779 . 2 (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
63, 4, 53imtr4i 199 1 (DECID 𝜑DECID ¬ 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 662  DECID wdc 778
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 779
This theorem is referenced by:  pm5.18dc  813  pm4.67dc  817  pm2.54dc  826  imordc  832  pm4.54dc  841  stabtestimpdc  860  annimdc  881  pm4.55dc  882  orandc  883  pm3.12dc  902  pm3.13dc  903  dn1dc  904  xor3dc  1321  dfbi3dc  1331  dcned  2257  gcdaddm  10900
  Copyright terms: Public domain W3C validator