This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )