Theorem pm3.24

Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Conclusion
\( \vdash \neg (\varphi \wedge \neg \varphi) \)
Proof
l0
id
\( \vdash \varphi \rightarrow \varphi \)
iman
\( \vdash \varphi \rightarrow \varphi \leftrightarrow \neg (\varphi \wedge \neg \varphi) \)
mpbi l0 _