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

Theorem dcn 828
 Description: The negation of a decidable proposition is decidable. The converse need not hold, but does hold for negated propositions, see dcnn 834. (Contributed by Jim Kingdon, 25-Mar-2018.)
Assertion
Ref Expression
dcn (DECID 𝜑DECID ¬ 𝜑)

Proof of Theorem dcn
StepHypRef Expression
1 notnot 619 . . . 4 (𝜑 → ¬ ¬ 𝜑)
21orim2i 751 . . 3 ((¬ 𝜑𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
32orcoms 720 . 2 ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4 df-dc 821 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5 df-dc 821 . 2 (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
63, 4, 53imtr4i 200 1 (DECID 𝜑DECID ¬ 𝜑)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 698  DECID wdc 820 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 604  ax-in2 605  ax-io 699 This theorem depends on definitions:  df-bi 116  df-dc 821 This theorem is referenced by:  stdcndc  831  stdcndcOLD  832  dcnn  834  pm5.18dc  869  pm4.67dc  873  pm2.54dc  877  imordc  883  pm4.54dc  888  annimdc  922  pm4.55dc  923  orandc  924  pm3.12dc  943  pm3.13dc  944  dn1dc  945  xor3dc  1369  dfbi3dc  1379  dcned  2333  gcdaddm  11848
 Copyright terms: Public domain W3C validator