Theorem 19.41v

Description: Version of 19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

	Ref	Expression
Assertion	19.41v	$$⊢\exists x\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\phi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.40	$$⊢\exists x\left(\phi \wedge \psi \right)\to \left(\exists x\phi \wedge \exists x\psi \right)$$
2		ax5e	$$⊢\exists x\psi \to \psi$$
3	2	anim2i	$$⊢\left(\exists x\phi \wedge \exists x\psi \right)\to \left(\exists x\phi \wedge \psi \right)$$
4	1 3	syl	$$⊢\exists x\left(\phi \wedge \psi \right)\to \left(\exists x\phi \wedge \psi \right)$$
5		pm3.21	$$⊢\psi \to \left(\phi \to \left(\phi \wedge \psi \right)\right)$$
6	5	eximdv	$$⊢\psi \to \left(\exists x\phi \to \exists x\left(\phi \wedge \psi \right)\right)$$
7	6	impcom	$$⊢\left(\exists x\phi \wedge \psi \right)\to \exists x\left(\phi \wedge \psi \right)$$
8	4 7	impbii	$$⊢\exists x\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\phi \wedge \psi \right)$$