Theorem pm5.19

Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)

Conclusion
\( \vdash \neg (\varphi \leftrightarrow \neg \varphi) \)
Proof
l0
biid
\( \vdash \varphi \leftrightarrow \varphi \)
pm5.18
\( \vdash \varphi \leftrightarrow \varphi \leftrightarrow \neg (\varphi \leftrightarrow \neg \varphi) \)
mpbi l0 _