Theorem pm2.01i

Inference associated with the weak Clavius law pm2.01. (Contributed by BJ, 30-Mar-2020.)

Hypothesis
pm2.01i.1
\( \vdash \varphi \rightarrow \neg \varphi \)
Conclusion
\( \vdash \neg \varphi \)
Proof
l0
pm2.01i.1
\( \vdash \varphi \rightarrow \neg \varphi \)
pm2.01
\( \vdash (\varphi \rightarrow \neg \varphi) \rightarrow \neg \varphi \)
ax-mp l0 _