Theorem dcn 844

Description: The negation of a decidable proposition is decidable. The converse need not hold, but does hold for negated propositions, see dcnn 850. (Contributed by Jim Kingdon, 25-Mar-2018.)

Assertion

Ref	Expression
dcn	⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Proof of Theorem dcn

Step	Hyp	Ref	Expression
1		notnot 630	. . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑)
2	1	orim2i 763	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 732	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 837	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 837	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 201	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 710  DECID wdc 836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711

This theorem depends on definitions:  df-bi 117  df-dc 837

This theorem is referenced by:  stdcndc  847  stdcndcOLD  848  dcnn  850  pm5.18dc  885  pm4.67dc  889  pm2.54dc  893  imordc  899  pm4.54dc  904  annimdc  940  pm4.55dc  941  orandc  942  pm3.12dc  961  pm3.13dc  962  dn1dc  963  xor3dc  1407  dfbi3dc  1417  dcned  2383  qdcle  10411  bitsdc  12333  gcdaddm  12380  prmdc  12527  pcmptdvds  12743  lgsquadlemofi  15628