Theorem dimatis

"Dimatis", one of the syllogisms of Aristotelian logic. Some \( \varphi \) is \( \psi \), and all \( \psi \) is \( \chi \), therefore some \( \chi \) is \( \varphi \). In Aristotelian notation, IAI-4: PiM and MaS therefore SiP. For example, "Some pets are rabbits", "All rabbits have fur", therefore "Some fur bearing animals are pets". Like darii with positions interchanged. (Contributed by David A. Wheeler, 28-Aug-2016.) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

Hypotheses
dimatis.maj
\( \vdash \exists x \, (\varphi \wedge \psi) \)
dimatis.min
\( \vdash \forall x \, (\psi \rightarrow \chi) \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \varphi) \)
Proof
l0
dimatis.min
\( \vdash \forall x \, (\psi \rightarrow \chi) \)
dimatis.maj
\( \vdash \exists x \, (\varphi \wedge \psi) \)
l2
darii l0 _
\( \vdash \exists x \, (\varphi \wedge \chi) \)
exancom
\( \vdash \exists x \, (\varphi \wedge \chi) \leftrightarrow \exists x \, (\chi \wedge \varphi) \)
mpbi l2 _