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 
|- ( ( ph <-> ( ps /\ -. ph ) ) -> -. ps )

Proof

Step Hyp Ref Expression
1 ibar 
 |-  ( ps -> ( -. ph <-> ( ps /\ -. ph ) ) )
2 nbbn 
 |-  ( ( -. ph <-> ( ps /\ -. ph ) ) <-> -. ( ph <-> ( ps /\ -. ph ) ) )
3 1 2 sylib 
 |-  ( ps -> -. ( ph <-> ( ps /\ -. ph ) ) )
4 3 con2i 
 |-  ( ( ph <-> ( ps /\ -. ph ) ) -> -. ps )