Description: A closed form of syllogism (see syl ). Theorem *2.05 of
WhiteheadRussell p. 100. Its associated inference is imim2i . Its
associated deduction is imim2d . An alternate proof from more basic
results is given by ax-1 followed by a2d . (Contributed by NM, 29-Dec-1992)(Proof shortened by Wolf Lammen, 6-Sep-2012)