Theorem barbarilem

Lemma for barbari and the other Aristotelian syllogisms with existential assumption. (Contributed by BJ, 16-Sep-2022.)

Hypotheses
barbarilem.min
\( \vdash \exists x \, \varphi \)
barbarilem.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
Conclusion
\( \vdash \exists x \, (\varphi \wedge \psi) \)
Proof
l0
barbarilem.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
l1
barbarilem.min
\( \vdash \exists x \, \varphi \)
exintr
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists x \, \varphi \rightarrow \exists x \, (\varphi \wedge \psi) \)
mp2 l0 l1 _