Theorem exintr

Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) (Proof shortened by BJ, 16-Sep-2022.)

Conclusion

\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists x \, \varphi \rightarrow \exists x \, (\varphi \wedge \psi) \)

Proof

ancl

aleximi _