Theorem calemos 2197

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 1582	. . . . 5 |- ( ps -> -. ch )
4	3	con2i 630	. . . 4 |- ( ch -> -. ps )
5		calemos.maj	. . . . 5 |- A. x ( ph -> ps )
6	5	spi 1582	. . . 4 |- ( ph -> ps )
7	4, 6	nsyl 631	. . 3 |- ( ch -> -. ph )
8	7	ancli 323	. 2 |- ( ch -> ( ch /\ -. ph ) )
9	1, 8	eximii 1648	1 |- E. x ( ch /\ -. ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   A.wal 1393   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by: (None)