This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )