ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dcn Unicode 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  ph  -> DECID  -.  ph )

Proof of Theorem dcn
StepHypRef Expression
1 notnot 619 . . . 4  |-  ( ph  ->  -.  -.  ph )
21orim2i 751 . . 3  |-  ( ( -.  ph  \/  ph )  ->  ( -.  ph  \/  -.  -.  ph ) )
32orcoms 720 . 2  |-  ( (
ph  \/  -.  ph )  ->  ( -.  ph  \/  -.  -.  ph ) )
4 df-dc 821 . 2  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
5 df-dc 821 . 2  |-  (DECID  -.  ph  <->  ( -.  ph  \/  -.  -.  ph ) )
63, 4, 53imtr4i 200 1  |-  (DECID  ph  -> DECID  -.  ph )
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  11884  prmdc  12023
  Copyright terms: Public domain W3C validator