This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )