Metamath Proof Explorer

Theorem pm5.55

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

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

Proof

Step Hyp Ref Expression
1 biort 
 |-  ( ph -> ( ph <-> ( ph \/ ps ) ) )
2 1 bicomd 
 |-  ( ph -> ( ( ph \/ ps ) <-> ph ) )
3 biorf 
 |-  ( -. ph -> ( ps <-> ( ph \/ ps ) ) )
4 3 bicomd 
 |-  ( -. ph -> ( ( ph \/ ps ) <-> ps ) )
5 2 4 nsyl5 
 |-  ( -. ( ( ph \/ ps ) <-> ph ) -> ( ( ph \/ ps ) <-> ps ) )
6 5 orri 
 |-  ( ( ( ph \/ ps ) <-> ph ) \/ ( ( ph \/ ps ) <-> ps ) )