Negation elimination

In symbolic logic, a valid inference in a system of truth-functional rules. This rule relies on the truth definition of the negation, where a doubly negated statement (¬¬P) is truth functionally equivalent to the statement (P) without the negations. (See also Double negation.)