Theorem exintrbi

Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)

Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow (\exists x \, \varphi \leftrightarrow \exists x \, (\varphi \wedge \psi)) \)
Proof
abai
rbaibr _
alexbii _