Metamath Proof Explorer

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 ⊢ ∀ x φ → ψ
darapti.min ⊢ ∀ x φ → χ
darapti.e ⊢ ∃ x φ
Assertion darapti ⊢ ∃ x χ ∧ ψ

Proof

Step Hyp Ref Expression
1 darapti.maj ⊢ ∀ x φ → ψ
2 darapti.min ⊢ ∀ x φ → χ
3 darapti.e ⊢ ∃ x φ
4 id ⊢ φ → χ ∧ φ → ψ → φ → χ ∧ φ → ψ
5 4 alanimi ⊢ ∀ x φ → χ ∧ ∀ x φ → ψ → ∀ x φ → χ ∧ φ → ψ
6 2 1 5 mp2an ⊢ ∀ x φ → χ ∧ φ → ψ
7 pm3.43 ⊢ φ → χ ∧ φ → ψ → φ → χ ∧ ψ
8 7 alimi ⊢ ∀ x φ → χ ∧ φ → ψ → ∀ x φ → χ ∧ ψ
9 6 8 ax-mp ⊢ ∀ x φ → χ ∧ ψ
10 exim ⊢ ∀ x φ → χ ∧ ψ → ∃ x φ → ∃ x χ ∧ ψ
11 9 3 10 mp2 ⊢ ∃ x χ ∧ ψ