Description: Conjoin antecedents and consequents of two premises. This is the closed
theorem form of anim12d . Theorem *3.47 of WhiteheadRussell p. 113.
It was proved by Leibniz, and it evidently pleased him enough to call it
praeclarum theorema (splendid theorem). (Contributed by NM, 12-Aug-1993)(Proof shortened by Wolf Lammen, 7-Apr-2013)