Theorem barbari 2305

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.xch

Assertion

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

Proof of Theorem barbari

Step	Hyp	Ref	Expression
1		barbari.e	. 2 |- E.xch
2		barbari.maj	. . . . . 6 |- A.x(ph -> ps)
3		barbari.min	. . . . . 6 |- A.x(ch -> ph)
4	2, 3	barbara 2301	. . . . 5 |- A.x(ch -> ps)
5	4	spi 1753	. . . 4 |- (ch -> ps)
6	5	ancli 534	. . 3 |- (ch -> (ch /\ ps))
7	6	eximi 1576	. 2 |- (E.xch -> E.x(ch /\ ps))
8	1, 7	ax-mp 5	1 |- E.x(ch /\ ps)

Syntax hints:   -> wi 4   /\ wa 358  A.wal 1540  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542

This theorem is referenced by:  celaront  2306