Theorem fresison

Description: "Fresison", one of the syllogisms of Aristotelian logic. No ph is ps (PeM), and some ps is ch (MiS), therefore some ch is not ph (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)

	Ref	Expression
Hypotheses	fresison.maj	$$⊢\forall x\left(\phi \to \neg \psi \right)$$
	fresison.min	$$⊢\exists x\left(\psi \wedge \chi \right)$$
Assertion	fresison	$$⊢\exists x\left(\chi \wedge \neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		fresison.maj	$$⊢\forall x\left(\phi \to \neg \psi \right)$$
2		fresison.min	$$⊢\exists x\left(\psi \wedge \chi \right)$$
3		exancom	$$⊢\exists x\left(\psi \wedge \chi \right)\leftrightarrow \exists x\left(\chi \wedge \psi \right)$$
4	2 3	mpbi	$$⊢\exists x\left(\chi \wedge \psi \right)$$
5	1 4	festino	$$⊢\exists x\left(\chi \wedge \neg \phi \right)$$