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	|- A. x ( ph -> -. ps )
	fesapo.min	|- A. x ( ps -> ch )
	fesapo.e	|- E. x ps
Assertion	fesapo	|- E. x ( ch /\ -. ph )

Proof

Step	Hyp	Ref	Expression
1		fesapo.maj	|- A. x ( ph -> -. ps )
2		fesapo.min	|- A. x ( ps -> ch )
3		fesapo.e	|- E. x ps
4		con2	|- ( ( ph -> -. ps ) -> ( ps -> -. ph ) )
5	4	alimi	|- ( A. x ( ph -> -. ps ) -> A. x ( ps -> -. ph ) )
6	1 5	ax-mp	|- A. x ( ps -> -. ph )
7	6 2 3	felapton	|- E. x ( ch /\ -. ph )