Theorem dcn 854

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

Assertion

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

Proof of Theorem dcn

Step	Hyp	Ref	Expression
1		notnot 638	. . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑)
2	1	orim2i 773	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 742	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 847	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 847	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 201	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 720  DECID wdc 846

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 623  ax-in2 624  ax-io 721

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

This theorem is referenced by:  stdcndc  857  stdcndcOLD  858  dcnn  860  pm5.18dc  895  pm4.67dc  899  pm2.54dc  903  imordc  909  pm4.54dc  914  annimdc  950  pm4.55dc  951  orandc  952  pm3.12dc  971  pm3.13dc  972  dn1dc  973  ifpnst  1001  xor3dc  1436  dfbi3dc  1446  dcned  2426  qdcle  10659  hashfibclem  11260  bitsdc  12692  gcdaddm  12739  prmdc  12886  pcmptdvds  13102  ballotfilemdifcfi  13203  ballotfilemdifcfz  13205  ballotfilem2  13206  ballotfilembfi  13217  lgsquadlemofi  16109  konigsberglem5  16647