Theorem dcn 849

Description: The negation of a decidable proposition is decidable. The converse need not hold, but does hold for negated propositions, see dcnn 855. (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 768	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 737	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 842	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 842	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 201	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 715  DECID wdc 841

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 716

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

This theorem is referenced by:  stdcndc  852  stdcndcOLD  853  dcnn  855  pm5.18dc  890  pm4.67dc  894  pm2.54dc  898  imordc  904  pm4.54dc  909  annimdc  945  pm4.55dc  946  orandc  947  pm3.12dc  966  pm3.13dc  967  dn1dc  968  ifpnst  996  xor3dc  1431  dfbi3dc  1441  dcned  2408  qdcle  10505  bitsdc  12507  gcdaddm  12554  prmdc  12701  pcmptdvds  12917  lgsquadlemofi  15804