Metamath Proof Explorer


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