Theorem disamis

Description: "Disamis", one of the syllogisms of Aristotelian logic. Some ph is ps , and all ph is ch , therefore some ch is ps . In Aristotelian notation, IAI-3: MiP and MaS therefore SiP. (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

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