Metamath Proof Explorer

Theorem pm5.15

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

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

Proof

Step Hyp Ref Expression
1 xor3 
 |-  ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )
2 1 biimpi 
 |-  ( -. ( ph <-> ps ) -> ( ph <-> -. ps ) )
3 2 orri 
 |-  ( ( ph <-> ps ) \/ ( ph <-> -. ps ) )