Theorem datisi

"Datisi", one of the syllogisms of Aristotelian logic. All \( \varphi \) is \( \psi \), and some \( \varphi \) is \( \chi \), therefore some \( \chi \) is \( \psi \). 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.)

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