Theorem cesaro

"Cesaro", one of the syllogisms of Aristotelian logic. No \( \varphi \) is \( \psi \), all \( \chi \) is \( \psi \), and \( \chi \) exist, therefore some \( \chi \) is not \( \varphi \). In Aristotelian notation, EAO-2: PeM and SaM therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016.) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

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