Theorem pm5.16

Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.)

Conclusion
\( \vdash \neg ((\varphi \leftrightarrow \psi) \wedge (\varphi \leftrightarrow \neg \psi)) \)
Proof
pm5.18
l1
biimpi _
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \neg (\varphi \leftrightarrow \neg \psi) \)
imnan
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \neg (\varphi \leftrightarrow \neg \psi) \leftrightarrow \neg ((\varphi \leftrightarrow \psi) \wedge (\varphi \leftrightarrow \neg \psi)) \)
mpbi l1 _