Theorem celarent

"Celarent", one of the syllogisms of Aristotelian logic. No \( \varphi \) is \( \psi \), and all \( \chi \) is \( \varphi \), therefore no \( \chi \) is \( \psi \). Instance of barbara. In Aristotelian notation, EAE-1: MeP and SaM therefore SeP. For example, given the "No reptiles have fur" and "All snakes are reptiles", therefore "No snakes have fur". Example from https://en.wikipedia.org/wiki/Syllogism. (Contributed by David A. Wheeler, 24-Aug-2016.)

Hypotheses
celarent.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
celarent.min
\( \vdash \forall x \, (\chi \rightarrow \varphi) \)
Conclusion
\( \vdash \forall x \, (\chi \rightarrow \neg \psi) \)
Proof
l0
celarent.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
celarent.min
\( \vdash \forall x \, (\chi \rightarrow \varphi) \)
barbara l0 _