Theorem dcn 832

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

Assertion

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

Proof of Theorem dcn

Step	Hyp	Ref	Expression
1		notnot 619	. . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑)
2	1	orim2i 751	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 720	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 825	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 825	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 200	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 698  DECID wdc 824

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 604  ax-in2 605  ax-io 699

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

This theorem is referenced by:  stdcndc  835  stdcndcOLD  836  dcnn  838  pm5.18dc  873  pm4.67dc  877  pm2.54dc  881  imordc  887  pm4.54dc  892  annimdc  927  pm4.55dc  928  orandc  929  pm3.12dc  948  pm3.13dc  949  dn1dc  950  xor3dc  1377  dfbi3dc  1387  dcned  2342  gcdaddm  11917  prmdc  12062  pcmptdvds  12275