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

Theorem dcn 780
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 777 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5 df-dc 777 . 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 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:  pm5.18dc  811  pm4.67dc  815  pm2.54dc  824  imordc  830  pm4.54dc  839  stabtestimpdc  858  annimdc  879  pm4.55dc  880  orandc  881  pm3.12dc  900  pm3.13dc  901  dn1dc  902  xor3dc  1319  dfbi3dc  1329  dcned  2255  gcdaddm  10600
  Copyright terms: Public domain W3C validator