Negation elimination rule
= Negation elimination rule
{title2=$\dfrac{P\qquad\neg P}{\bot}$}
From a <propositional formula> and its <negation>, infer <logical falsity>. This identifies a contradiction inside a <natural deduction> derivation; a later <negation introduction rule> may discharge the assumption that led to it.