Theorem barbari

"Barbari", one of the syllogisms of Aristotelian logic. All \( \varphi \) is \( \psi \), all \( \chi \) is \( \varphi \), and some \( \chi \) exist, therefore some \( \chi \) is \( \psi \). 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
barbari.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
barbari.min
\( \vdash \forall x \, (\chi \rightarrow \varphi) \)
barbari.e
\( \vdash \exists x \, \chi \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \psi) \)
Proof
l0
barbari.e
l1
barbari.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
barbari.min
\( \vdash \forall x \, (\chi \rightarrow \varphi) \)
barbara l1 _
barbarilem l0 _