Metamath Proof Explorer


Theorem cesare

Description: "Cesare", one of the syllogisms of Aristotelian logic. No ph is ps , and all ch is ps , therefore no ch is ph . In Aristotelian notation, EAE-2: PeM and SaM therefore SeP. Related to celarent . (Contributed by David A. Wheeler, 27-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

Ref Expression
Hypotheses cesare.maj x φ ¬ ψ
cesare.min x χ ψ
Assertion cesare x χ ¬ φ

Proof

Step Hyp Ref Expression
1 cesare.maj x φ ¬ ψ
2 cesare.min x χ ψ
3 con2 φ ¬ ψ ψ ¬ φ
4 3 alimi x φ ¬ ψ x ψ ¬ φ
5 1 4 ax-mp x ψ ¬ φ
6 5 2 celarent x χ ¬ φ