Theorem r19.41dv

Description: A complex deduction form of r19.41v . (Contributed by Zhi Wang, 6-Sep-2024)

	Ref	Expression
Hypothesis	r19.41dv.1	$$⊢\phi \to \exists x\in A\psi$$
Assertion	r19.41dv	$$⊢\left(\phi \wedge \chi \right)\to \exists x\in A\left(\psi \wedge \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.41dv.1	$$⊢\phi \to \exists x\in A\psi$$
2	1	anim1i	$$⊢\left(\phi \wedge \chi \right)\to \left(\exists x\in A\psi \wedge \chi \right)$$
3		r19.41v	$$⊢\exists x\in A\left(\psi \wedge \chi \right)\leftrightarrow \left(\exists x\in A\psi \wedge \chi \right)$$
4	2 3	sylibr	$$⊢\left(\phi \wedge \chi \right)\to \exists x\in A\left(\psi \wedge \chi \right)$$