Theorem pclem6

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

	Ref	Expression
Assertion	pclem6	$$⊢\left(\phi \leftrightarrow \left(\psi \wedge \neg \phi \right)\right)\to \neg \psi$$

Proof

Step	Hyp	Ref	Expression
1		ibar	$$⊢\psi \to \left(\neg \phi \leftrightarrow \left(\psi \wedge \neg \phi \right)\right)$$
2		nbbn	$$⊢\left(\neg \phi \leftrightarrow \left(\psi \wedge \neg \phi \right)\right)\leftrightarrow \neg \left(\phi \leftrightarrow \left(\psi \wedge \neg \phi \right)\right)$$
3	1 2	sylib	$$⊢\psi \to \neg \left(\phi \leftrightarrow \left(\psi \wedge \neg \phi \right)\right)$$
4	3	con2i	$$⊢\left(\phi \leftrightarrow \left(\psi \wedge \neg \phi \right)\right)\to \neg \psi$$