Theorem darapti 2709

Description: "Darapti", one of the syllogisms of Aristotelian logic. All 𝜑 is 𝜓, all 𝜑 is 𝜒, and some 𝜑 exist, therefore some 𝜒 is 𝜓. 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.)

Hypotheses

Ref	Expression
darapti.maj	⊢ ∀𝑥(𝜑 → 𝜓)
darapti.min	⊢ ∀𝑥(𝜑 → 𝜒)
darapti.e	⊢ ∃𝑥𝜑

Assertion

Ref	Expression
darapti	⊢ ∃𝑥(𝜒 ∧ 𝜓)

Proof of Theorem darapti

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  felapton  2711