Theorem dcn 757

Description: A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.)

Assertion

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

Proof of Theorem dcn

Step	Hyp	Ref	Expression
1		notnot 569	. . . 4 ⊢ (𝜑 → ¬ ¬ 𝜑)
2	1	orim2i 688	. . 3 ⊢ ((¬ 𝜑 ∨ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
3	2	orcoms 659	. 2 ⊢ ((𝜑 ∨ ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
4		df-dc 754	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
5		df-dc 754	. 2 ⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
6	3, 4, 5	3imtr4i 194	1 ⊢ (DECID 𝜑 → DECID ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 639  DECID wdc 753

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640

This theorem depends on definitions:  df-bi 114  df-dc 754

This theorem is referenced by:  pm5.18dc  788  pm4.67dc  792  pm2.54dc  801  imordc  807  pm4.54dc  816  stabtestimpdc  835  annimdc  856  pm4.55dc  857  pm3.12dc  876  pm3.13dc  877  dn1dc  878  xor3dc  1294  dfbi3dc  1304  dcned  2226