Theorem fesapo

Description: "Fesapo", one of the syllogisms of Aristotelian logic. No ph is ps , all ps is ch , and ps exist, therefore some ch is not ph . In Aristotelian notation, EAO-4: PeM and MaS therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		fesapo.maj	$$⊢\forall x\left(\phi \to \neg \psi \right)$$
2		fesapo.min	$$⊢\forall x\left(\psi \to \chi \right)$$
3		fesapo.e	$$⊢\exists x\psi$$
4		con2	$$⊢\left(\phi \to \neg \psi \right)\to \left(\psi \to \neg \phi \right)$$
5	4	alimi	$$⊢\forall x\left(\phi \to \neg \psi \right)\to \forall x\left(\psi \to \neg \phi \right)$$
6	1 5	ax-mp	$$⊢\forall x\left(\psi \to \neg \phi \right)$$
7	6 2 3	felapton	$$⊢\exists x\left(\chi \wedge \neg \phi \right)$$