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  10681  hashfibclem  11282  bitsdc  12714  gcdaddm  12761  prmdc  12908  pcmptdvds  13124  ballotfilemdifcfi  13225  ballotfilemdifcfz  13227  ballotfilem2  13228  ballotfilembfi  13239  lgsquadlemofi  16195  konigsberglem5  16733