MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  calemos Structured version   Unicode version

Theorem calemos 2401
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
StepHypRef Expression
1 calemos.e . 2  |-  E. x ch
2 calemos.min . . . . . 6  |-  A. x
( ps  ->  -.  ch )
32spi 1799 . . . . 5  |-  ( ps 
->  -.  ch )
43con2i 120 . . . 4  |-  ( ch 
->  -.  ps )
5 calemos.maj . . . . 5  |-  A. x
( ph  ->  ps )
65spi 1799 . . . 4  |-  ( ph  ->  ps )
74, 6nsyl 121 . . 3  |-  ( ch 
->  -.  ph )
87ancli 551 . 2  |-  ( ch 
->  ( ch  /\  -.  ph ) )
91, 8eximii 1627 1  |-  E. x
( ch  /\  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369   A.wal 1367   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator