Theorem dcn 810

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

Assertion

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

Proof of Theorem dcn

Step	Hyp	Ref	Expression
1		notnot 601	. . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑)
2	1	orim2i 733	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 702	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 803	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 803	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 200	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 680  DECID wdc 802

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681

This theorem depends on definitions:  df-bi 116  df-dc 803

This theorem is referenced by:  stdcndc  813  stdcndcOLD  814  dcnn  816  pm5.18dc  849  pm4.67dc  853  pm2.54dc  857  imordc  863  pm4.54dc  868  annimdc  902  pm4.55dc  903  orandc  904  pm3.12dc  923  pm3.13dc  924  dn1dc  925  xor3dc  1346  dfbi3dc  1356  dcned  2286  gcdaddm  11514