Theorem festino

Description: "Festino", one of the syllogisms of Aristotelian logic. No ph is ps , and some ch is ps , therefore some ch is not ph . In Aristotelian notation, EIO-2: PeM and SiM therefore SoP. (Contributed by David A. Wheeler, 25-Nov-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

	Ref	Expression
Hypotheses	festino.maj	|- A. x ( ph -> -. ps )
	festino.min	|- E. x ( ch /\ ps )
Assertion	festino	|- E. x ( ch /\ -. ph )

Proof

Step	Hyp	Ref	Expression
1		festino.maj	|- A. x ( ph -> -. ps )
2		festino.min	|- E. x ( ch /\ ps )
3		con2	|- ( ( ph -> -. ps ) -> ( ps -> -. ph ) )
4	3	anim2d	|- ( ( ph -> -. ps ) -> ( ( ch /\ ps ) -> ( ch /\ -. ph ) ) )
5	4	alimi	|- ( A. x ( ph -> -. ps ) -> A. x ( ( ch /\ ps ) -> ( ch /\ -. ph ) ) )
6	1 5	ax-mp	|- A. x ( ( ch /\ ps ) -> ( ch /\ -. ph ) )
7		exim	|- ( A. x ( ( ch /\ ps ) -> ( ch /\ -. ph ) ) -> ( E. x ( ch /\ ps ) -> E. x ( ch /\ -. ph ) ) )
8	6 2 7	mp2	|- E. x ( ch /\ -. ph )