This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (φ \leftrightarrow (ψ \land \neg φ)) \to \neg ψ$

Step	Hyp	Ref	Expression
1		ibar	$⊢ ψ \to (\neg φ \leftrightarrow (ψ \land \neg φ))$
2		nbbn	$⊢ (\neg φ \leftrightarrow (ψ \land \neg φ)) \leftrightarrow \neg (φ \leftrightarrow (ψ \land \neg φ))$
3	1 2	sylib	$⊢ ψ \to \neg (φ \leftrightarrow (ψ \land \neg φ))$
4	3	con2i	$⊢ (φ \leftrightarrow (ψ \land \neg φ)) \to \neg ψ$