Description: Theorem *13.13 in WhiteheadRussell p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011)