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	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
	darapti.min	⊢ ∀ 𝑥 ( 𝜑 → 𝜒 )
	darapti.e	⊢ ∃ 𝑥 𝜑
Assertion	darapti	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		darapti.maj	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
2		darapti.min	⊢ ∀ 𝑥 ( 𝜑 → 𝜒 )
3		darapti.e	⊢ ∃ 𝑥 𝜑
4		id	⊢ ( ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) → ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) )
5	4	alanimi	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜒 ) ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) → ∀ 𝑥 ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) )
6	2 1 5	mp2an	⊢ ∀ 𝑥 ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) )
7		pm3.43	⊢ ( ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )
8	7	alimi	⊢ ( ∀ 𝑥 ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) → ∀ 𝑥 ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )
9	6 8	ax-mp	⊢ ∀ 𝑥 ( 𝜑 → ( 𝜒 ∧ 𝜓 ) )
10		exim	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝜒 ∧ 𝜓 ) ) )
11	9 3 10	mp2	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )