Description: A syllogism rule of inference. The second premise is used to replace
the consequent of the first premise. Copy of syl6 with a different
proof. (Contributed by Wolf Lammen, 17-Dec-2018)(New usage is discouraged.)(Proof modification is discouraged.)