Theorem baroco

Description: "Baroco", one of the syllogisms of Aristotelian logic. All ph is ps , and some ch is not ps , therefore some ch is not ph . In Aristotelian notation, AOO-2: PaM and SoM therefore SoP. For example, "All informative things are useful", "Some websites are not useful", therefore "Some websites are not informative". (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		baroco.maj	|- A. x ( ph -> ps )
2		baroco.min	|- E. x ( ch /\ -. ps )
3		con3	|- ( ( 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 )