Theorem dcn 850

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

Assertion

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

Proof of Theorem dcn

Step	Hyp	Ref	Expression
1		notnot 634	. . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑)
2	1	orim2i 769	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 738	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 843	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 843	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 201	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 716  DECID wdc 842

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 619  ax-in2 620  ax-io 717

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

This theorem is referenced by:  stdcndc  853  stdcndcOLD  854  dcnn  856  pm5.18dc  891  pm4.67dc  895  pm2.54dc  899  imordc  905  pm4.54dc  910  annimdc  946  pm4.55dc  947  orandc  948  pm3.12dc  967  pm3.13dc  968  dn1dc  969  ifpnst  997  xor3dc  1432  dfbi3dc  1442  dcned  2409  qdcle  10552  bitsdc  12571  gcdaddm  12618  prmdc  12765  pcmptdvds  12981  lgsquadlemofi  15878  konigsberglem5  16416