Description: "Disamis", one of the syllogisms of Aristotelian logic. Some ph is
ps , and all ph is ch , therefore some ch is ps .
In Aristotelian notation, IAI-3: MiP and MaS therefore SiP.
(Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on
axioms. (Revised by BJ, 16-Sep-2022)