Description: Lemma for iscnrm3lem5 and iscnrm3r . (Contributed by Zhi Wang, 4-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iscnrm3lem4.1 | ⊢ ( 𝜂 → ( 𝜓 → 𝜁 ) ) | |
iscnrm3lem4.2 | ⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) → 𝜂 ) | ||
iscnrm3lem4.3 | ⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜃 ) → ( 𝜁 → 𝜏 ) ) | ||
Assertion | iscnrm3lem4 | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃 → 𝜏 ) ) ) ) |
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 | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃 → 𝜏 ) ) ) ) |