Step |
Hyp |
Ref |
Expression |
1 |
|
iscnrm3lem2.1 |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 → ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) ) |
2 |
|
iscnrm3lem2.2 |
⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐷 ∀ 𝑣 ∈ 𝐸 𝜒 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) ) |
3 |
|
2ax5 |
⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) → ∀ 𝑤 ∀ 𝑣 ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) |
4 |
|
r3al |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) |
5 |
4 1
|
syl5bir |
⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) → ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) ) |
6 |
5
|
2alimdv |
⊢ ( 𝜑 → ( ∀ 𝑤 ∀ 𝑣 ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) → ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) ) |
7 |
3 6
|
syl5 |
⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) → ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) ) |
8 |
|
2ax5 |
⊢ ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) |
9 |
8
|
alrimiv |
⊢ ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) |
10 |
|
r2al |
⊢ ( ∀ 𝑤 ∈ 𝐷 ∀ 𝑣 ∈ 𝐸 𝜒 ↔ ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) |
11 |
10 2
|
syl5bir |
⊢ ( 𝜑 → ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) ) |
12 |
11
|
2alimdv |
⊢ ( 𝜑 → ( ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) ) |
13 |
12
|
alimdv |
⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) ) |
14 |
9 13
|
syl5 |
⊢ ( 𝜑 → ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) ) |
15 |
7 14
|
impbid |
⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ↔ ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) ) |
16 |
15 4 10
|
3bitr4g |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 ↔ ∀ 𝑤 ∈ 𝐷 ∀ 𝑣 ∈ 𝐸 𝜒 ) ) |