Metamath Proof Explorer


Theorem calemos

Description: "Calemos", one of the syllogisms of Aristotelian logic. All ph is ps (PaM), no ps is ch (MeS), and ch exist, therefore some ch is not ph (SoP). In Aristotelian notation, AEO-4: PaM and MeS therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

Ref Expression
Hypotheses calemos.maj
|- A. x ( ph -> ps )
calemos.min
|- A. x ( ps -> -. ch )
calemos.e
|- E. x ch
Assertion calemos
|- E. x ( ch /\ -. ph )

Proof

Step Hyp Ref Expression
1 calemos.maj
 |-  A. x ( ph -> ps )
2 calemos.min
 |-  A. x ( ps -> -. ch )
3 calemos.e
 |-  E. x ch
4 1 2 calemes
 |-  A. x ( ch -> -. ph )
5 3 4 barbarilem
 |-  E. x ( ch /\ -. ph )