Clavius' Law

Consequentia mirabilis (Latin for "admirable consequence"), also known as Clavius's Law, is used in traditional and classical logic to establish the truth of a proposition from the inconsistency of its negation. It is thus similar to reductio ad absurdum, but it can prove a proposition true using just its negation. It states that if a proposition is a consequence of its negation, then it is true, for consistency. It can thus be demonstrated without using any other principle, but that of consistency. (Barnes claims in passing that the term 'consequentia mirabilis' refers only to the inference of the proposition from the inconsistency of its negation, and that the term 'Lex Clavia' (or Clavius' Law) refers to the inference of the proposition's negation from the inconsistency of the proposition.)

In formal notation: ${\displaystyle (\neg A\rightarrow A)\rightarrow A}$ which is equivalent to ${\displaystyle (\neg \neg A\lor A)\rightarrow A}$.

...
Wikipedia