Theorem calemos

"Calemos", one of the syllogisms of Aristotelian logic. All \( \varphi \) is \( \psi \) (PaM), no \( \psi \) is \( \chi \) (MeS), and \( \chi \) exist, therefore some \( \chi \) is not \( \varphi \) (SoP). In Aristotelian notation, AEO-4: PaM and MeS therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016.) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

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