Step |
Hyp |
Ref |
Expression |
1 |
|
2stdpc4 |
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) |
2 |
1
|
gen2 |
⊢ ∀ 𝑡 ∀ 𝑧 ( ∀ 𝑥 ∀ 𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) |
3 |
|
nfv |
⊢ Ⅎ 𝑡 𝜑 |
4 |
3
|
nfal |
⊢ Ⅎ 𝑡 ∀ 𝑦 𝜑 |
5 |
4
|
nfal |
⊢ Ⅎ 𝑡 ∀ 𝑥 ∀ 𝑦 𝜑 |
6 |
|
nfv |
⊢ Ⅎ 𝑧 𝜑 |
7 |
6
|
nfal |
⊢ Ⅎ 𝑧 ∀ 𝑦 𝜑 |
8 |
7
|
nfal |
⊢ Ⅎ 𝑧 ∀ 𝑥 ∀ 𝑦 𝜑 |
9 |
5 8
|
2stdpc5 |
⊢ ( ∀ 𝑡 ∀ 𝑧 ( ∀ 𝑥 ∀ 𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) → ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑡 ∀ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) ) |
10 |
2 9
|
ax-mp |
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑡 ∀ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) |
11 |
6
|
nfsbv |
⊢ Ⅎ 𝑧 [ 𝑡 / 𝑦 ] 𝜑 |
12 |
11
|
sb8v |
⊢ ( ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) |
13 |
12
|
albii |
⊢ ( ∀ 𝑡 ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 ↔ ∀ 𝑡 ∀ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ) |
14 |
10 13
|
sylibr |
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑡 ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 ) |
15 |
|
sbal |
⊢ ( [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 ) |
16 |
15
|
albii |
⊢ ( ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑡 ∀ 𝑥 [ 𝑡 / 𝑦 ] 𝜑 ) |
17 |
14 16
|
sylibr |
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 ) |
18 |
3
|
nfal |
⊢ Ⅎ 𝑡 ∀ 𝑥 𝜑 |
19 |
18
|
sb8v |
⊢ ( ∀ 𝑦 ∀ 𝑥 𝜑 ↔ ∀ 𝑡 [ 𝑡 / 𝑦 ] ∀ 𝑥 𝜑 ) |
20 |
17 19
|
sylibr |
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) |