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
|- A. x ( ph -> ps )
darii.min
|- E. x ( ch /\ ph )
Assertion darii
|- E. x ( ch /\ ps )

Proof

Step Hyp Ref Expression
1 darii.maj
 |-  A. x ( ph -> ps )
2 darii.min
 |-  E. x ( ch /\ ph )
3 id
 |-  ( ( ph -> ps ) -> ( ph -> ps ) )
4 3 anim2d
 |-  ( ( ph -> ps ) -> ( ( ch /\ ph ) -> ( ch /\ ps ) ) )
5 4 alimi
 |-  ( A. x ( ph -> ps ) -> A. x ( ( ch /\ ph ) -> ( ch /\ ps ) ) )
6 1 5 ax-mp
 |-  A. x ( ( ch /\ ph ) -> ( ch /\ ps ) )
7 exim
 |-  ( A. x ( ( ch /\ ph ) -> ( ch /\ ps ) ) -> ( E. x ( ch /\ ph ) -> E. x ( ch /\ ps ) ) )
8 6 2 7 mp2
 |-  E. x ( ch /\ ps )