Theorem ferison

"Ferison", one of the syllogisms of Aristotelian logic. No \( \varphi \) is \( \psi \), and some \( \varphi \) is \( \chi \), therefore some \( \chi \) is not \( \psi \). Instance of datisi. In Aristotelian notation, EIO-3: MeP and MiS therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016.)

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