Proof of Theorem r3al
Step | Hyp | Ref
| Expression |
1 | | df-ral 2453 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
2 | | r2al 2489 |
. . 3
⊢
(∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)) |
3 | 2 | ralbii 2476 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)) |
4 | | 3anass 977 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶))) |
5 | 4 | imbi1i 237 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜑)) |
6 | | impexp 261 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜑) ↔ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
7 | 5, 6 | bitri 183 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ↔ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
8 | 7 | albii 1463 |
. . . . . 6
⊢
(∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ↔ ∀𝑧(𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
9 | | 19.21v 1866 |
. . . . . 6
⊢
(∀𝑧(𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
10 | 8, 9 | bitri 183 |
. . . . 5
⊢
(∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
11 | 10 | albii 1463 |
. . . 4
⊢
(∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ↔ ∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
12 | | 19.21v 1866 |
. . . 4
⊢
(∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
13 | 11, 12 | bitri 183 |
. . 3
⊢
(∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
14 | 13 | albii 1463 |
. 2
⊢
(∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))) |
15 | 1, 3, 14 | 3bitr4i 211 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)) |