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	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )