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

Theorem barbari 2347
Description: "Barbari", one of the syllogisms of Aristotelian logic. All  ph is  ps, all  ch is  ph, and some  ch exist, therefore some  ch is  ps. (In Aristotelian notation, AAI-1: MaP and SaM therefore SiP.) For example, given "All men are mortal", "All Greeks are men", and "Greeks exist", therefore "Some Greeks are mortal". Note the existence hypothesis (to prove the "some" in the conclusion). Example from https://en.wikipedia.org/wiki/Syllogism. (Contributed by David A. Wheeler, 27-Aug-2016.) (Revised by David A. Wheeler, 30-Aug-2016.)
Hypotheses
Ref Expression
barbari.maj  |-  A. x
( ph  ->  ps )
barbari.min  |-  A. x
( ch  ->  ph )
barbari.e  |-  E. x ch
Assertion
Ref Expression
barbari  |-  E. x
( ch  /\  ps )

Proof of Theorem barbari
StepHypRef Expression
1 barbari.e . 2  |-  E. x ch
2 barbari.maj . . . . 5  |-  A. x
( ph  ->  ps )
3 barbari.min . . . . 5  |-  A. x
( ch  ->  ph )
42, 3barbara 2343 . . . 4  |-  A. x
( ch  ->  ps )
54spi 1890 . . 3  |-  ( ch 
->  ps )
65ancli 551 . 2  |-  ( ch 
->  ( ch  /\  ps ) )
71, 6eximii 1681 1  |-  E. x
( ch  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1405   E.wex 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-12 1880
This theorem depends on definitions:  df-bi 187  df-an 371  df-ex 1636
This theorem is referenced by:  celaront  2348
  Copyright terms: Public domain W3C validator