Theorem dimatis 2582

Description: "Dimatis", one of the syllogisms of Aristotelian logic. Some ph is ps, and all ps is ch, therefore some ch is ph. (In Aristotelian notation, IAI-4: PiM and MaS therefore SiP.) For example, "Some pets are rabbits.", "All rabbits have fur", therefore "Some fur bearing animals are pets". Like darii 2565 with positions interchanged. (Contributed by David A. Wheeler, 28-Aug-2016.)

Hypotheses

Ref	Expression
dimatis.maj	|- E. x ( ph /\ ps )
dimatis.min	|- A. x ( ps -> ch )

Assertion

Ref	Expression
dimatis	|- E. x ( ch /\ ph )

Proof of Theorem dimatis

Step	Hyp	Ref	Expression
1		dimatis.maj	. 2 |- E. x ( ph /\ ps )
2		dimatis.min	. . . . 5 |- A. x ( ps -> ch )
3	2	spi 2054	. . . 4 |- ( ps -> ch )
4	3	adantl 482	. . 3 |- ( ( ph /\ ps ) -> ch )
5		simpl 473	. . 3 |- ( ( ph /\ ps ) -> ph )
6	4, 5	jca 554	. 2 |- ( ( ph /\ ps ) -> ( ch /\ ph ) )
7	1, 6	eximii 1764	1 |- E. x ( ch /\ ph )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by: (None)