Theorem disamis

"Disamis", one of the syllogisms of Aristotelian logic. Some \( \varphi \) is \( \psi \), and all \( \varphi \) is \( \chi \), therefore some \( \chi \) is \( \psi \). 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.)

Hypotheses
disamis.maj
\( \vdash \exists x \, (\varphi \wedge \psi) \)
disamis.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \psi) \)
Proof
l0
disamis.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
disamis.maj
\( \vdash \exists x \, (\varphi \wedge \psi) \)
l2
datisi l0 _
\( \vdash \exists x \, (\psi \wedge \chi) \)
exancom
\( \vdash \exists x \, (\psi \wedge \chi) \leftrightarrow \exists x \, (\chi \wedge \psi) \)
mpbi l2 _