Theorem iscnrm3lem7

Description: Lemma for iscnrm3rlem8 and iscnrm3llem2 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Hypotheses	iscnrm3lem7.1	|- ( z = Z -> ( ch <-> th ) )
	iscnrm3lem7.2	|- ( w = W -> ( th <-> ta ) )
	iscnrm3lem7.3	|- ( ( ph /\ ( x e. A /\ y e. B ) /\ ps ) -> ( Z e. C /\ W e. D /\ ta ) )
Assertion	iscnrm3lem7	|- ( ph -> ( E. x e. A E. y e. B ps -> E. z e. C E. w e. D ch ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3lem7.1	|- ( z = Z -> ( ch <-> th ) )
2		iscnrm3lem7.2	|- ( w = W -> ( th <-> ta ) )
3		iscnrm3lem7.3	|- ( ( ph /\ ( x e. A /\ y e. B ) /\ ps ) -> ( Z e. C /\ W e. D /\ ta ) )
4	1 2	rspc2ev	|- ( ( Z e. C /\ W e. D /\ ta ) -> E. z e. C E. w e. D ch )
5	3 4	syl	|- ( ( ph /\ ( x e. A /\ y e. B ) /\ ps ) -> E. z e. C E. w e. D ch )
6	5	iscnrm3lem6	|- ( ph -> ( E. x e. A E. y e. B ps -> E. z e. C E. w e. D ch ) )