Metamath Proof Explorer

Theorem pm5.62

Description: Theorem *5.62 of WhiteheadRussell p. 125. (Contributed by Roy F. Longton, 21-Jun-2005)

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

Proof

Step Hyp Ref Expression
1 exmid 
 |-  ( ps \/ -. ps )
2 ordir 
 |-  ( ( ( ph /\ ps ) \/ -. ps ) <-> ( ( ph \/ -. ps ) /\ ( ps \/ -. ps ) ) )
3 1 2 mpbiran2 
 |-  ( ( ( ph /\ ps ) \/ -. ps ) <-> ( ph \/ -. ps ) )