Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr . (Contributed by NM, 29-Dec-1992) (Proof shortened by Wolf Lammen, 16-Sep-2013)