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