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

Metamath Proof Explorer

Theorem pm5.16

Description: Theorem *5.16 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 17-Oct-2013)

Ref Expression
Assertion pm5.16 
|- -. ( ( ph <-> ps ) /\ ( ph <-> -. ps ) )

Proof

Step Hyp Ref Expression
1 pm5.18 
 |-  ( ( ph <-> ps ) <-> -. ( ph <-> -. ps ) )
2 1 biimpi 
 |-  ( ( ph <-> ps ) -> -. ( ph <-> -. ps ) )
3 imnan 
 |-  ( ( ( ph <-> ps ) -> -. ( ph <-> -. ps ) ) <-> -. ( ( ph <-> ps ) /\ ( ph <-> -. ps ) ) )
4 2 3 mpbi 
 |-  -. ( ( ph <-> ps ) /\ ( ph <-> -. ps ) )