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 𝑥 ( 𝜑𝜓 )
barbari.min 𝑥 ( 𝜒𝜑 )
barbari.e 𝑥 𝜒
Assertion barbari 𝑥 ( 𝜒𝜓 )

Proof

Step Hyp Ref Expression
1 barbari.maj 𝑥 ( 𝜑𝜓 )
2 barbari.min 𝑥 ( 𝜒𝜑 )
3 barbari.e 𝑥 𝜒
4 1 2 barbara 𝑥 ( 𝜒𝜓 )
5 3 4 barbarilem 𝑥 ( 𝜒𝜓 )