Theorem dcn 837

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

Assertion

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

Proof of Theorem dcn

Step	Hyp	Ref	Expression
1		notnot 624	. . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑)
2	1	orim2i 756	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 725	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 830	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 830	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 200	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 703  DECID wdc 829

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

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

This theorem is referenced by:  stdcndc  840  stdcndcOLD  841  dcnn  843  pm5.18dc  878  pm4.67dc  882  pm2.54dc  886  imordc  892  pm4.54dc  897  annimdc  932  pm4.55dc  933  orandc  934  pm3.12dc  953  pm3.13dc  954  dn1dc  955  xor3dc  1382  dfbi3dc  1392  dcned  2346  gcdaddm  11939  prmdc  12084  pcmptdvds  12297