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

Metamath Proof Explorer

Theorem pm5.17

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

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

Proof

Step Hyp Ref Expression
1 bicom 
 |-  ( ( ph <-> -. ps ) <-> ( -. ps <-> ph ) )
2 dfbi2 
 |-  ( ( -. ps <-> ph ) <-> ( ( -. ps -> ph ) /\ ( ph -> -. ps ) ) )
3 orcom 
 |-  ( ( ph \/ ps ) <-> ( ps \/ ph ) )
4 df-or 
 |-  ( ( ps \/ ph ) <-> ( -. ps -> ph ) )
5 3 4 bitr2i 
 |-  ( ( -. ps -> ph ) <-> ( ph \/ ps ) )
6 imnan 
 |-  ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )
7 5 6 anbi12i 
 |-  ( ( ( -. ps -> ph ) /\ ( ph -> -. ps ) ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
8 1 2 7 3bitrri 
 |-  ( ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) <-> ( ph <-> -. ps ) )