Metamath Proof Explorer


Theorem dimatis

Description: "Dimatis", one of the syllogisms of Aristotelian logic. Some ph is ps , and all ps is ch , therefore some ch is ph . 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 with positions interchanged. (Contributed by David A. Wheeler, 28-Aug-2016) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

Ref Expression
Hypotheses dimatis.maj
|- E. x ( ph /\ ps )
dimatis.min
|- A. x ( ps -> ch )
Assertion dimatis
|- E. x ( ch /\ ph )

Proof

Step Hyp Ref Expression
1 dimatis.maj
 |-  E. x ( ph /\ ps )
2 dimatis.min
 |-  A. x ( ps -> ch )
3 2 1 darii
 |-  E. x ( ph /\ ch )
4 exancom
 |-  ( E. x ( ph /\ ch ) <-> E. x ( ch /\ ph ) )
5 3 4 mpbi
 |-  E. x ( ch /\ ph )