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

Theorem dimatis 2415
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 2398 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 1864 . . . 4
43adantl 466 . . 3
5 simpl 457 . . 3
64, 5jca 532 . 2
71, 6eximii 1658 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  A.wal 1393  E.wex 1612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613
  Copyright terms: Public domain W3C validator