Theorem dcn 847

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

Assertion

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

Proof of Theorem dcn

Step	Hyp	Ref	Expression
1		notnot 632	. . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑)
2	1	orim2i 766	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 735	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 840	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 840	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 201	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 713  DECID wdc 839

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 617  ax-in2 618  ax-io 714

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

This theorem is referenced by:  stdcndc  850  stdcndcOLD  851  dcnn  853  pm5.18dc  888  pm4.67dc  892  pm2.54dc  896  imordc  902  pm4.54dc  907  annimdc  943  pm4.55dc  944  orandc  945  pm3.12dc  964  pm3.13dc  965  dn1dc  966  ifpnst  994  xor3dc  1429  dfbi3dc  1439  dcned  2406  qdcle  10461  bitsdc  12453  gcdaddm  12500  prmdc  12647  pcmptdvds  12863  lgsquadlemofi  15749