Metamath Proof Explorer


Theorem iscnrm3lem4

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

Ref Expression
Hypotheses iscnrm3lem4.1 ( 𝜂 → ( 𝜓𝜁 ) )
iscnrm3lem4.2 ( ( 𝜑𝜒𝜃 ) → 𝜂 )
iscnrm3lem4.3 ( ( 𝜑𝜒𝜃 ) → ( 𝜁𝜏 ) )
Assertion iscnrm3lem4 ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃𝜏 ) ) ) )

Proof

Step Hyp Ref Expression
1 iscnrm3lem4.1 ( 𝜂 → ( 𝜓𝜁 ) )
2 iscnrm3lem4.2 ( ( 𝜑𝜒𝜃 ) → 𝜂 )
3 iscnrm3lem4.3 ( ( 𝜑𝜒𝜃 ) → ( 𝜁𝜏 ) )
4 iscnrm3lem3 ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜒𝜃 ) ∧ 𝜓 ) )
5 2 1 syl ( ( 𝜑𝜒𝜃 ) → ( 𝜓𝜁 ) )
6 5 3 syld ( ( 𝜑𝜒𝜃 ) → ( 𝜓𝜏 ) )
7 6 imp ( ( ( 𝜑𝜒𝜃 ) ∧ 𝜓 ) → 𝜏 )
8 4 7 sylbi ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) → 𝜏 )
9 8 exp43 ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃𝜏 ) ) ) )