This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 darapti.maj 
 |-  A. x ( ph -> ps )
2 darapti.min 
 |-  A. x ( ph -> ch )
3 darapti.e 
 |-  E. x ph
4 id 
 |-  ( ( ( ph -> ch ) /\ ( ph -> ps ) ) -> ( ( ph -> ch ) /\ ( ph -> ps ) ) )
5 4 alanimi 
 |-  ( ( A. x ( ph -> ch ) /\ A. x ( ph -> ps ) ) -> A. x ( ( ph -> ch ) /\ ( ph -> ps ) ) )
6 2 1 5 mp2an 
 |-  A. x ( ( ph -> ch ) /\ ( ph -> ps ) )
7 pm3.43 
 |-  ( ( ( ph -> ch ) /\ ( ph -> ps ) ) -> ( ph -> ( ch /\ ps ) ) )
8 7 alimi 
 |-  ( A. x ( ( ph -> ch ) /\ ( ph -> ps ) ) -> A. x ( ph -> ( ch /\ ps ) ) )
9 6 8 ax-mp 
 |-  A. x ( ph -> ( ch /\ ps ) )
10 exim 
 |-  ( A. x ( ph -> ( ch /\ ps ) ) -> ( E. x ph -> E. x ( ch /\ ps ) ) )
11 9 3 10 mp2 
 |-  E. x ( ch /\ ps )