Description: More general version of 3imtr3i . Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996) (Proof shortened by Wolf Lammen, 20-Dec-2013)