Theorem r19.41dv

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

	Ref	Expression
Hypothesis	r19.41dv.1	|- ( ph -> E. x e. A ps )
Assertion	r19.41dv	|- ( ( ph /\ ch ) -> E. x e. A ( ps /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		r19.41dv.1	|- ( ph -> E. x e. A ps )
2	1	anim1i	|- ( ( ph /\ ch ) -> ( E. x e. A ps /\ ch ) )
3		r19.41v	|- ( E. x e. A ( ps /\ ch ) <-> ( E. x e. A ps /\ ch ) )
4	2 3	sylibr	|- ( ( ph /\ ch ) -> E. x e. A ( ps /\ ch ) )