Theorem iscnrm3lem5

Description: Lemma for iscnrm3l . (Contributed by Zhi Wang, 3-Sep-2024)

	Ref	Expression
Hypotheses	iscnrm3lem5.1	|- ( ( x = S /\ y = T ) -> ( ph <-> ps ) )
	iscnrm3lem5.2	|- ( ( x = S /\ y = T ) -> ( ch <-> th ) )
	iscnrm3lem5.3	|- ( ( ta /\ et /\ ze ) -> ( S e. V /\ T e. W ) )
	iscnrm3lem5.4	|- ( ( ta /\ et /\ ze ) -> ( ( ps -> th ) -> si ) )
Assertion	iscnrm3lem5	|- ( ta -> ( A. x e. V A. y e. W ( ph -> ch ) -> ( et -> ( ze -> si ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3lem5.1	|- ( ( x = S /\ y = T ) -> ( ph <-> ps ) )
2		iscnrm3lem5.2	|- ( ( x = S /\ y = T ) -> ( ch <-> th ) )
3		iscnrm3lem5.3	|- ( ( ta /\ et /\ ze ) -> ( S e. V /\ T e. W ) )
4		iscnrm3lem5.4	|- ( ( ta /\ et /\ ze ) -> ( ( ps -> th ) -> si ) )
5	1 2	imbi12d	|- ( ( x = S /\ y = T ) -> ( ( ph -> ch ) <-> ( ps -> th ) ) )
6	5	rspc2gv	|- ( ( S e. V /\ T e. W ) -> ( A. x e. V A. y e. W ( ph -> ch ) -> ( ps -> th ) ) )
7	6 3 4	iscnrm3lem4	|- ( ta -> ( A. x e. V A. y e. W ( ph -> ch ) -> ( et -> ( ze -> si ) ) ) )