Theorem calemos 2133

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.) (Revised by David A. Wheeler, 2-Sep-2016.)

Hypotheses

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

Assertion

Ref	Expression
calemos	|- E. x ( ch /\ -. ph )

Proof of Theorem calemos

Step	Hyp	Ref	Expression
1		calemos.e	. 2 |- E. x ch
2		calemos.min	. . . . . 6 |- A. x ( ps -> -. ch )
3	2	spi 1524	. . . . 5 |- ( ps -> -. ch )
4	3	con2i 617	. . . 4 |- ( ch -> -. ps )
5		calemos.maj	. . . . 5 |- A. x ( ph -> ps )
6	5	spi 1524	. . . 4 |- ( ph -> ps )
7	4, 6	nsyl 618	. . 3 |- ( ch -> -. ph )
8	7	ancli 321	. 2 |- ( ch -> ( ch /\ -. ph ) )
9	1, 8	eximii 1590	1 |- E. x ( ch /\ -. ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   A.wal 1341   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by: (None)