Theorem pm2.18

Clavius law, or "consequentia mirabilis" ("admirable consequence"). If a formula is implied by its negation, then it is true. Can be used in proofs by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. See also the weak Clavius law pm2.01. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 17-Nov-2023.)

Conclusion
\( \vdash (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
Proof
id
pm2.18d _