Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of WhiteheadRussell p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003)