Metamath Proof Explorer


Theorem fesapo

Description: "Fesapo", one of the syllogisms of Aristotelian logic. No ph is ps , all ps is ch , and ps exist, therefore some ch is not ph . In Aristotelian notation, EAO-4: PeM and MaS therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

Step Hyp Ref Expression
1 fesapo.maj x φ ¬ ψ
2 fesapo.min x ψ χ
3 fesapo.e x ψ
4 con2 φ ¬ ψ ψ ¬ φ
5 4 alimi x φ ¬ ψ x ψ ¬ φ
6 1 5 ax-mp x ψ ¬ φ
7 6 2 3 felapton x χ ¬ φ