Theorem calemos 2584

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 2054	. . . . 5 |- ( ps -> -. ch )
4	3	con2i 134	. . . 4 |- ( ch -> -. ps )
5		calemos.maj	. . . . 5 |- A. x ( ph -> ps )
6	5	spi 2054	. . . 4 |- ( ph -> ps )
7	4, 6	nsyl 135	. . 3 |- ( ch -> -. ph )
8	7	ancli 574	. 2 |- ( ch -> ( ch /\ -. ph ) )
9	1, 8	eximii 1764	1 |- E. x ( ch /\ -. ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by: (None)