Theorem iscnrm3lem4

Description: Lemma for iscnrm3lem5 and iscnrm3r . (Contributed by Zhi Wang, 4-Sep-2024)

	Ref	Expression
Hypotheses	iscnrm3lem4.1	|- ( et -> ( ps -> ze ) )
	iscnrm3lem4.2	|- ( ( ph /\ ch /\ th ) -> et )
	iscnrm3lem4.3	|- ( ( ph /\ ch /\ th ) -> ( ze -> ta ) )
Assertion	iscnrm3lem4	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3lem4.1	|- ( et -> ( ps -> ze ) )
2		iscnrm3lem4.2	|- ( ( ph /\ ch /\ th ) -> et )
3		iscnrm3lem4.3	|- ( ( ph /\ ch /\ th ) -> ( ze -> ta ) )
4		iscnrm3lem3	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch /\ th ) /\ ps ) )
5	2 1	syl	|- ( ( ph /\ ch /\ th ) -> ( ps -> ze ) )
6	5 3	syld	|- ( ( ph /\ ch /\ th ) -> ( ps -> ta ) )
7	6	imp	|- ( ( ( ph /\ ch /\ th ) /\ ps ) -> ta )
8	4 7	sylbi	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
9	8	exp43	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )