Deduction adding nested antecedents. Deduction associated with imim2 and imim2i. (Contributed by NM, 10-Jan-1993.)