Theorem pm2.18i

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

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