Double Negation (DN for short) is a rule of inference used in Propositional Logic.
¬ ¬P = P ('Not not P' = 'P')
Back up to Rules of Inference Review your Logic symbols