Theorem barbari 2189

Description: "Barbari", one of the syllogisms of Aristotelian logic. All 𝜑 is 𝜓, all 𝜒 is 𝜑, and some 𝜒 exist, therefore some 𝜒 is 𝜓. (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	⊢ ∀𝑥(𝜑 → 𝜓)
barbari.min	⊢ ∀𝑥(𝜒 → 𝜑)
barbari.e	⊢ ∃𝑥𝜒

Assertion

Ref	Expression
barbari	⊢ ∃𝑥(𝜒 ∧ 𝜓)

Proof of Theorem barbari

Step	Hyp	Ref	Expression
1		barbari.e	. 2 ⊢ ∃𝑥𝜒
2		barbari.maj	. . . . 5 ⊢ ∀𝑥(𝜑 → 𝜓)
3		barbari.min	. . . . 5 ⊢ ∀𝑥(𝜒 → 𝜑)
4	2, 3	barbara 2185	. . . 4 ⊢ ∀𝑥(𝜒 → 𝜓)
5	4	spi 1589	. . 3 ⊢ (𝜒 → 𝜓)
6	5	ancli 323	. 2 ⊢ (𝜒 → (𝜒 ∧ 𝜓))
7	1, 6	eximii 1655	1 ⊢ ∃𝑥(𝜒 ∧ 𝜓)

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1400  ∃wex 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  celaront  2190