Metamath Proof Explorer


Theorem camestres

Description: "Camestres", one of the syllogisms of Aristotelian logic. All ph is ps , and no ch is ps , therefore no ch is ph . In Aristotelian notation, AEE-2: PaM and SeM therefore SeP. (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

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