Theorem bijust0

A self-implication (see id) does not imply its own negation. The justification theorem bijust is one of its instances. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) Extract bijust0 from proof of bijust. (Revised by BJ, 19-Mar-2020.)

Conclusion
\( \vdash \neg ((\varphi \rightarrow \varphi) \rightarrow \neg (\varphi \rightarrow \varphi)) \)
Proof
l0
id
\( \vdash \varphi \rightarrow \varphi \)
pm2.01
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \neg (\varphi \rightarrow \varphi)) \rightarrow \neg (\varphi \rightarrow \varphi) \)
mt2 l0 _