Description: Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of WhiteheadRussell p. 118. (Contributed by NM, 3-Jan-2005)