Description: Deduction that converts a biconditional implied by one of its arguments, into an implication. Deduction associated with ibi . (Contributed by NM, 26-Jun-2004)