Metamath Proof Explorer

Theorem darii

Description: "Darii", one of the syllogisms of Aristotelian logic. All ph is ps , and some ch is ph , therefore some ch is ps . In Aristotelian notation, AII-1: MaP and SiM therefore SiP. For example, given "All rabbits have fur" and "Some pets are rabbits", therefore "Some pets have fur". Example from https://en.wikipedia.org/wiki/Syllogism . See dariiALT for a shorter proof requiring more axioms. (Contributed by David A. Wheeler, 24-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

Ref Expression
Hypotheses darii.maj ⊢ ∀ x φ → ψ
darii.min ⊢ ∃ x χ ∧ φ
Assertion darii ⊢ ∃ x χ ∧ ψ

Proof

Step Hyp Ref Expression
1 darii.maj ⊢ ∀ x φ → ψ
2 darii.min ⊢ ∃ x χ ∧ φ
3 id ⊢ φ → ψ → φ → ψ
4 3 anim2d ⊢ φ → ψ → χ ∧ φ → χ ∧ ψ
5 4 alimi ⊢ ∀ x φ → ψ → ∀ x χ ∧ φ → χ ∧ ψ
6 1 5 ax-mp ⊢ ∀ x χ ∧ φ → χ ∧ ψ
7 exim ⊢ ∀ x χ ∧ φ → χ ∧ ψ → ∃ x χ ∧ φ → ∃ x χ ∧ ψ
8 6 2 7 mp2 ⊢ ∃ x χ ∧ ψ