Description: Lemma for iscnrm3l . (Contributed by Zhi Wang, 3-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iscnrm3lem5.1 | ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑇 ) → ( 𝜑 ↔ 𝜓 ) ) | |
iscnrm3lem5.2 | ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑇 ) → ( 𝜒 ↔ 𝜃 ) ) | ||
iscnrm3lem5.3 | ⊢ ( ( 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) ) | ||
iscnrm3lem5.4 | ⊢ ( ( 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( ( 𝜓 → 𝜃 ) → 𝜎 ) ) | ||
Assertion | iscnrm3lem5 | ⊢ ( 𝜏 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 ( 𝜑 → 𝜒 ) → ( 𝜂 → ( 𝜁 → 𝜎 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscnrm3lem5.1 | ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑇 ) → ( 𝜑 ↔ 𝜓 ) ) | |
2 | iscnrm3lem5.2 | ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑇 ) → ( 𝜒 ↔ 𝜃 ) ) | |
3 | iscnrm3lem5.3 | ⊢ ( ( 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) ) | |
4 | iscnrm3lem5.4 | ⊢ ( ( 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( ( 𝜓 → 𝜃 ) → 𝜎 ) ) | |
5 | 1 2 | imbi12d | ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑇 ) → ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) ) ) |
6 | 5 | rspc2gv | ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 ( 𝜑 → 𝜒 ) → ( 𝜓 → 𝜃 ) ) ) |
7 | 6 3 4 | iscnrm3lem4 | ⊢ ( 𝜏 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 ( 𝜑 → 𝜒 ) → ( 𝜂 → ( 𝜁 → 𝜎 ) ) ) ) |