---
tags:
  - Logic
  - propositional-logic
  - derivation-rules
---

This is also known as *proof by contradiction*. You start with an assumption declared in a subproof. If you can derive a contradiction from this assumption (typically from the introduction of another proposition and its negation), then you are permitted to derive the negation of the auxiliary assumption in the main proof. 

[]()![negate-intro 1.png](../img/negate-intro%201.png)