Theorem celaront

"Celaront", one of the syllogisms of Aristotelian logic. No \( \varphi \) is \( \psi \), all \( \chi \) is \( \varphi \), and some \( \chi \) exist, therefore some \( \chi \) is not \( \psi \). Instance of barbari. In Aristotelian notation, EAO-1: MeP and SaM therefore SoP. For example, given "No reptiles have fur", "All snakes are reptiles", and "Snakes exist", prove "Some snakes have no fur". Note the existence hypothesis. Example from https://en.wikipedia.org/wiki/Syllogism. (Contributed by David A. Wheeler, 27-Aug-2016.)

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