Description: Theorem *5.11 of WhiteheadRussell p. 123. (Contributed by NM, 3-Jan-2005)
|- ( ( ph -> ps ) \/ ( -. ph -> ps ) )