Theorem barbari 2002

Description: "Barbari", one of the syllogisms of Aristotelian logic. All ph is ps, all ch is ph, and some ch exist, therefore some ch is ps. (In Aristotelian notation, AAI-1: MaP and SaM therefore SiP.) For example, given "All men are mortal", "All Greeks are men", and "Greeks exist", therefore "Some Greeks are mortal". Note the existence hypothesis (to prove the "some" in the conclusion). Example from https://en.wikipedia.org/wiki/Syllogism. (Contributed by David A. Wheeler, 27-Aug-2016.) (Revised by David A. Wheeler, 30-Aug-2016.)

Hypotheses

Ref	Expression
barbari.maj	|- A. x ( ph -> ps )
barbari.min	|- A. x ( ch -> ph )
barbari.e	|- E. x ch

Assertion

Ref	Expression
barbari	|- E. x ( ch /\ ps )

Proof of Theorem barbari

Step	Hyp	Ref	Expression
1		barbari.e	. 2 |- E. x ch
2		barbari.maj	. . . . 5 |- A. x ( ph -> ps )
3		barbari.min	. . . . 5 |- A. x ( ch -> ph )
4	2, 3	barbara 1998	. . . 4 |- A. x ( ch -> ps )
5	4	spi 1429	. . 3 |- ( ch -> ps )
6	5	ancli 306	. 2 |- ( ch -> ( ch /\ ps ) )
7	1, 6	eximii 1493	1 |- E. x ( ch /\ ps )

Syntax hints:   -> wi 4   /\ wa 97   A.wal 1241   E.wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  celaront  2003