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 ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 720  DECID wdc 846

This proof depends on 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 proof depends on definitions:  df-bi 117  df-dc 847

This theorem is used 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  10691  hashfibclem  11296  bitsdc  12730  gcdaddm  12777  prmdc  12924  pcmptdvds  13144  ballotfilemdifcfi  13274  ballotfilemdifcfz  13276  ballotfilem2  13277  ballotfilembfi  13288  lgsquadlemofi  16293  konigsberglem5  16831