Description: "Datisi", one of the syllogisms of Aristotelian logic. All ph is
ps , and some ph is ch , therefore some ch is ps .
In Aristotelian notation, AII-3: MaP and MiS therefore SiP.
(Contributed by David A. Wheeler, 28-Aug-2016) Shorten and reduce
dependencies on axioms. (Revised by BJ, 16-Sep-2022)