Theorem fresison

"Fresison", one of the syllogisms of Aristotelian logic. No \( \varphi \) is \( \psi \) (PeM), and some \( \psi \) is \( \chi \) (MiS), therefore some \( \chi \) is not \( \varphi \) (SoP). In Aristotelian notation, EIO-4: PeM and MiS therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016.) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

Hypotheses
fresison.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
fresison.min
\( \vdash \exists x \, (\psi \wedge \chi) \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \neg \varphi) \)
Proof
l0
fresison.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
l1
fresison.min
\( \vdash \exists x \, (\psi \wedge \chi) \)
exancom
\( \vdash \exists x \, (\psi \wedge \chi) \leftrightarrow \exists x \, (\chi \wedge \psi) \)
mpbi l1 _
\( \vdash \exists x \, (\chi \wedge \psi) \)
festino l0 _