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	⊢ ( ( 𝜑 ↔ ( 𝜓 ∧ ¬ 𝜑 ) ) → ¬ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ibar	⊢ ( 𝜓 → ( ¬ 𝜑 ↔ ( 𝜓 ∧ ¬ 𝜑 ) ) )
2		nbbn	⊢ ( ( ¬ 𝜑 ↔ ( 𝜓 ∧ ¬ 𝜑 ) ) ↔ ¬ ( 𝜑 ↔ ( 𝜓 ∧ ¬ 𝜑 ) ) )
3	1 2	sylib	⊢ ( 𝜓 → ¬ ( 𝜑 ↔ ( 𝜓 ∧ ¬ 𝜑 ) ) )
4	3	con2i	⊢ ( ( 𝜑 ↔ ( 𝜓 ∧ ¬ 𝜑 ) ) → ¬ 𝜓 )