Theorem bamalip

Description: "Bamalip", one of the syllogisms of Aristotelian logic. All ph is ps , all ps is ch , and ph exist, therefore some ch is ph . In Aristotelian notation, AAI-4: PaM and MaS therefore SiP. Very similar to barbari . (Contributed by David A. Wheeler, 28-Aug-2016) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

	Ref	Expression
Hypotheses	bamalip.maj	$$⊢\forall x\left(\phi \to \psi \right)$$
	bamalip.min	$$⊢\forall x\left(\psi \to \chi \right)$$
	bamalip.e	$$⊢\exists x\phi$$
Assertion	bamalip	$$⊢\exists x\left(\chi \wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bamalip.maj	$$⊢\forall x\left(\phi \to \psi \right)$$
2		bamalip.min	$$⊢\forall x\left(\psi \to \chi \right)$$
3		bamalip.e	$$⊢\exists x\phi$$
4	2 1 3	barbari	$$⊢\exists x\left(\phi \wedge \chi \right)$$
5		exancom	$$⊢\exists x\left(\phi \wedge \chi \right)\leftrightarrow \exists x\left(\chi \wedge \phi \right)$$
6	4 5	mpbi	$$⊢\exists x\left(\chi \wedge \phi \right)$$