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χ∧ψ