Theorem camestros

"Camestros", one of the syllogisms of Aristotelian logic. All \( \varphi \) is \( \psi \), no \( \chi \) is \( \psi \), and \( \chi \) exist, therefore some \( \chi \) is not \( \varphi \). In Aristotelian notation, AEO-2: PaM and SeM therefore SoP. For example, "All horses have hooves", "No humans have hooves", and humans exist, therefore "Some humans are not horses". (Contributed by David A. Wheeler, 28-Aug-2016.) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

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