Metamath Proof Explorer

Theorem pm5.61

Description: Theorem *5.61 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 30-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 orel2 
 |-  ( -. ps -> ( ( ph \/ ps ) -> ph ) )
2 orc 
 |-  ( ph -> ( ph \/ ps ) )
3 1 2 impbid1 
 |-  ( -. ps -> ( ( ph \/ ps ) <-> ph ) )
4 3 pm5.32ri 
 |-  ( ( ( ph \/ ps ) /\ -. ps ) <-> ( ph /\ -. ps ) )