Theorem pclem6

Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi \wedge \neg \varphi) \rightarrow \neg \psi \)
Proof
l0
ibar
\( \vdash \psi \rightarrow (\neg \varphi \leftrightarrow \psi \wedge \neg \varphi) \)
nbbn
\( \vdash \neg \varphi \leftrightarrow \psi \wedge \neg \varphi \leftrightarrow \neg (\varphi \leftrightarrow \psi \wedge \neg \varphi) \)
sylib l0 _
con2i _