Theorem bocardo

"Bocardo", one of the syllogisms of Aristotelian logic. Some \( \varphi \) is not \( \psi \), and all \( \varphi \) is \( \chi \), therefore some \( \chi \) is not \( \psi \). Instance of disamis. In Aristotelian notation, OAO-3: MoP and MaS therefore SoP. For example, "Some cats have no tails", "All cats are mammals", therefore "Some mammals have no tails". (Contributed by David A. Wheeler, 28-Aug-2016.)

Hypotheses
bocardo.maj
\( \vdash \exists x \, (\varphi \wedge \neg \psi) \)
bocardo.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \neg \psi) \)
Proof
l0
bocardo.maj
\( \vdash \exists x \, (\varphi \wedge \neg \psi) \)
bocardo.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
disamis l0 _