Step |
Hyp |
Ref |
Expression |
1 |
|
bj-cbv1hv.1 |
|- ( ph -> ( ps -> A. y ps ) ) |
2 |
|
bj-cbv1hv.2 |
|- ( ph -> ( ch -> A. x ch ) ) |
3 |
|
bj-cbv1hv.3 |
|- ( ph -> ( x = y -> ( ps -> ch ) ) ) |
4 |
|
nfa1 |
|- F/ x A. x A. y ph |
5 |
|
nfa2 |
|- F/ y A. x A. y ph |
6 |
|
2sp |
|- ( A. x A. y ph -> ph ) |
7 |
6 1
|
syl |
|- ( A. x A. y ph -> ( ps -> A. y ps ) ) |
8 |
5 7
|
nf5d |
|- ( A. x A. y ph -> F/ y ps ) |
9 |
6 2
|
syl |
|- ( A. x A. y ph -> ( ch -> A. x ch ) ) |
10 |
4 9
|
nf5d |
|- ( A. x A. y ph -> F/ x ch ) |
11 |
6 3
|
syl |
|- ( A. x A. y ph -> ( x = y -> ( ps -> ch ) ) ) |
12 |
4 5 8 10 11
|
cbv1v |
|- ( A. x A. y ph -> ( A. x ps -> A. y ch ) ) |