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 φψ¬φ¬ψ

Proof

Step Hyp Ref Expression
1 ibar ψ¬φψ¬φ
2 nbbn ¬φψ¬φ¬φψ¬φ
3 1 2 sylib ψ¬φψ¬φ
4 3 con2i φψ¬φ¬ψ