---
tags:
  - logic
  - propositional-logic
---

# Negation Elimination

Like the [introduction](Negation_Introduction.md) rule for
negation, the elimination rule also works by deriving a contradiction. It is
basically _Negation Introduction_ in reverse. Instead of starting the sub-proof
with a true proposition from which you derive a contradiction, you start with
the negation of a proposition, derive a contradiction and then assert the
positive of the negated proposition you started out with.

![](static/negate-elim.png)