Metamath Proof Explorer


Theorem barbari

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

Ref Expression
Hypotheses barbari.maj xφψ
barbari.min xχφ
barbari.e xχ
Assertion barbari xχψ

Proof

Step Hyp Ref Expression
1 barbari.maj xφψ
2 barbari.min xχφ
3 barbari.e xχ
4 1 2 barbara xχψ
5 3 4 barbarilem xχψ