Theorem barbari 2696

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.) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

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	. . 3 ⊢ ∀𝑥(𝜑 → 𝜓)
3		barbari.min	. . 3 ⊢ ∀𝑥(𝜒 → 𝜑)
4	2, 3	barbara 2690	. 2 ⊢ ∀𝑥(𝜒 → 𝜓)
5	1, 4	barbarilem 2695	1 ⊢ ∃𝑥(𝜒 ∧ 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  celaront  2698  bamalip  2719