Theorem celaront

Description: "Celaront", one of the syllogisms of Aristotelian logic. No ph is ps , all ch is ph , and some ch exist, therefore some ch is not ps . Instance of barbari . In Aristotelian notation, EAO-1: MeP and SaM therefore SoP. For example, given "No reptiles have fur", "All snakes are reptiles", and "Snakes exist", prove "Some snakes have no fur". Note the existence hypothesis. Example from https://en.wikipedia.org/wiki/Syllogism . (Contributed by David A. Wheeler, 27-Aug-2016)

	Ref	Expression
Hypotheses	celaront.maj	⊢ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 )
	celaront.min	⊢ ∀ 𝑥 ( 𝜒 → 𝜑 )
	celaront.e	⊢ ∃ 𝑥 𝜒
Assertion	celaront	⊢ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		celaront.maj	⊢ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 )
2		celaront.min	⊢ ∀ 𝑥 ( 𝜒 → 𝜑 )
3		celaront.e	⊢ ∃ 𝑥 𝜒
4	1 2 3	barbari	⊢ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜓 )