Metamath Proof Explorer


Theorem iscnrm3lem5

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

Ref Expression
Hypotheses iscnrm3lem5.1 x=Sy=Tφψ
iscnrm3lem5.2 x=Sy=Tχθ
iscnrm3lem5.3 τηζSVTW
iscnrm3lem5.4 τηζψθσ
Assertion iscnrm3lem5 τxVyWφχηζσ

Proof

Step Hyp Ref Expression
1 iscnrm3lem5.1 x=Sy=Tφψ
2 iscnrm3lem5.2 x=Sy=Tχθ
3 iscnrm3lem5.3 τηζSVTW
4 iscnrm3lem5.4 τηζψθσ
5 1 2 imbi12d x=Sy=Tφχψθ
6 5 rspc2gv SVTWxVyWφχψθ
7 6 3 4 iscnrm3lem4 τxVyWφχηζσ