MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dimatis Structured version   Visualization version   GIF version

Theorem dimatis 2569
Description: "Dimatis", one of the syllogisms of Aristotelian logic. Some 𝜑 is 𝜓, and all 𝜓 is 𝜒, therefore some 𝜒 is 𝜑. (In Aristotelian notation, IAI-4: PiM and MaS therefore SiP.) For example, "Some pets are rabbits.", "All rabbits have fur", therefore "Some fur bearing animals are pets". Like darii 2552 with positions interchanged. (Contributed by David A. Wheeler, 28-Aug-2016.)
Hypotheses
Ref Expression
dimatis.maj 𝑥(𝜑𝜓)
dimatis.min 𝑥(𝜓𝜒)
Assertion
Ref Expression
dimatis 𝑥(𝜒𝜑)

Proof of Theorem dimatis
StepHypRef Expression
1 dimatis.maj . 2 𝑥(𝜑𝜓)
2 dimatis.min . . . . 5 𝑥(𝜓𝜒)
32spi 2040 . . . 4 (𝜓𝜒)
43adantl 480 . . 3 ((𝜑𝜓) → 𝜒)
5 simpl 471 . . 3 ((𝜑𝜓) → 𝜑)
64, 5jca 552 . 2 ((𝜑𝜓) → (𝜒𝜑))
71, 6eximii 1753 1 𝑥(𝜒𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2032
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator