Theorem darapti

Description: "Darapti", one of the syllogisms of Aristotelian logic. All ph is ps , all ph is ch , and some ph exist, therefore some ch is ps . In Aristotelian notation, AAI-3: MaP and MaS therefore SiP. For example, "All squares are rectangles" and "All squares are rhombuses", therefore "Some rhombuses are rectangles". (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		darapti.maj	|- A. x ( ph -> ps )
2		darapti.min	|- A. x ( ph -> ch )
3		darapti.e	|- E. x ph
4		id	|- ( ( ( ph -> ch ) /\ ( ph -> ps ) ) -> ( ( ph -> ch ) /\ ( ph -> ps ) ) )
5	4	alanimi	|- ( ( A. x ( ph -> ch ) /\ A. x ( ph -> ps ) ) -> A. x ( ( ph -> ch ) /\ ( ph -> ps ) ) )
6	2 1 5	mp2an	|- A. x ( ( ph -> ch ) /\ ( ph -> ps ) )
7		pm3.43	|- ( ( ( ph -> ch ) /\ ( ph -> ps ) ) -> ( ph -> ( ch /\ ps ) ) )
8	7	alimi	|- ( A. x ( ( ph -> ch ) /\ ( ph -> ps ) ) -> A. x ( ph -> ( ch /\ ps ) ) )
9	6 8	ax-mp	|- A. x ( ph -> ( ch /\ ps ) )
10		exim	|- ( A. x ( ph -> ( ch /\ ps ) ) -> ( E. x ph -> E. x ( ch /\ ps ) ) )
11	9 3 10	mp2	|- E. x ( ch /\ ps )