Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Copy of imim1i with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018)