Proof of Theorem sbcom2v
Step | Hyp | Ref
| Expression |
1 | | alcom 1458 |
. . 3
⊢
(∀𝑧∀𝑥(𝑥 = 𝑦 → (𝑧 = 𝑤 → 𝜑)) ↔ ∀𝑥∀𝑧(𝑥 = 𝑦 → (𝑧 = 𝑤 → 𝜑))) |
2 | | bi2.04 247 |
. . . . . 6
⊢ ((𝑥 = 𝑦 → (𝑧 = 𝑤 → 𝜑)) ↔ (𝑧 = 𝑤 → (𝑥 = 𝑦 → 𝜑))) |
3 | 2 | albii 1450 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝑦 → (𝑧 = 𝑤 → 𝜑)) ↔ ∀𝑥(𝑧 = 𝑤 → (𝑥 = 𝑦 → 𝜑))) |
4 | | 19.21v 1853 |
. . . . 5
⊢
(∀𝑥(𝑧 = 𝑤 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
5 | 3, 4 | bitri 183 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → (𝑧 = 𝑤 → 𝜑)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
6 | 5 | albii 1450 |
. . 3
⊢
(∀𝑧∀𝑥(𝑥 = 𝑦 → (𝑧 = 𝑤 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
7 | | 19.21v 1853 |
. . . 4
⊢
(∀𝑧(𝑥 = 𝑦 → (𝑧 = 𝑤 → 𝜑)) ↔ (𝑥 = 𝑦 → ∀𝑧(𝑧 = 𝑤 → 𝜑))) |
8 | 7 | albii 1450 |
. . 3
⊢
(∀𝑥∀𝑧(𝑥 = 𝑦 → (𝑧 = 𝑤 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧(𝑧 = 𝑤 → 𝜑))) |
9 | 1, 6, 8 | 3bitr3i 209 |
. 2
⊢
(∀𝑧(𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧(𝑧 = 𝑤 → 𝜑))) |
10 | | sb6 1866 |
. . 3
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ ∀𝑧(𝑧 = 𝑤 → [𝑦 / 𝑥]𝜑)) |
11 | | sb6 1866 |
. . . . 5
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
12 | 11 | imbi2i 225 |
. . . 4
⊢ ((𝑧 = 𝑤 → [𝑦 / 𝑥]𝜑) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
13 | 12 | albii 1450 |
. . 3
⊢
(∀𝑧(𝑧 = 𝑤 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑧(𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
14 | 10, 13 | bitri 183 |
. 2
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ ∀𝑧(𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
15 | | sb6 1866 |
. . 3
⊢ ([𝑦 / 𝑥][𝑤 / 𝑧]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑤 / 𝑧]𝜑)) |
16 | | sb6 1866 |
. . . . 5
⊢ ([𝑤 / 𝑧]𝜑 ↔ ∀𝑧(𝑧 = 𝑤 → 𝜑)) |
17 | 16 | imbi2i 225 |
. . . 4
⊢ ((𝑥 = 𝑦 → [𝑤 / 𝑧]𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧(𝑧 = 𝑤 → 𝜑))) |
18 | 17 | albii 1450 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑦 → [𝑤 / 𝑧]𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧(𝑧 = 𝑤 → 𝜑))) |
19 | 15, 18 | bitri 183 |
. 2
⊢ ([𝑦 / 𝑥][𝑤 / 𝑧]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧(𝑧 = 𝑤 → 𝜑))) |
20 | 9, 14, 19 | 3bitr4i 211 |
1
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑) |