Double negation elimination
In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition A is logically equivalent to not (not-A), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.
Like the law of the excluded middle, this principle is considered to be a law of thought in classical logic, but it is disallowed by intuitionistic logic. The principle was stated as a theorem of propositional logic by Russell and Whitehead in Principia Mathematica as:
Double negative elimination (also called double negation elimination, double negative introduction, double negation introduction, double negation, or negation elimination) are two valid rules of replacement. They are the inferences that if A is true, then not not-A is true and its converse, that, if not not-A is true, then A is true. The rule allows one to introduce or eliminate a negation from a logical proof. The rule is based on the equivalence of, for example, It is false that it is not raining. and It is raining.
The double negation introduction rule is:
and the double negation elimination rule is:
Where "" is a metalogical symbol representing "can be replaced in a proof with."
...
Wikipedia