Theorem felapton

"Felapton", one of the syllogisms of Aristotelian logic. No \( \varphi \) is \( \psi \), all \( \varphi \) is \( \chi \), and some \( \varphi \) exist, therefore some \( \chi \) is not \( \psi \). Instance of darapti. In Aristotelian notation, EAO-3: MeP and MaS therefore SoP. For example, "No flowers are animals" and "All flowers are plants", therefore "Some plants are not animals". (Contributed by David A. Wheeler, 28-Aug-2016.)

Hypotheses
felapton.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
felapton.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
felapton.e
\( \vdash \exists x \, \varphi \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \neg \psi) \)
Proof
l0
felapton.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
l1
felapton.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
felapton.e
\( \vdash \exists x \, \varphi \)
darapti l0 l1 _