Step |
Hyp |
Ref |
Expression |
1 |
|
cbval2v.1 |
|- F/ z ph |
2 |
|
cbval2v.2 |
|- F/ w ph |
3 |
|
cbval2v.3 |
|- F/ x ps |
4 |
|
cbval2v.4 |
|- F/ y ps |
5 |
|
cbval2v.5 |
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) ) |
6 |
1
|
nfal |
|- F/ z A. y ph |
7 |
3
|
nfal |
|- F/ x A. w ps |
8 |
|
nfv |
|- F/ w x = z |
9 |
8 2
|
nfim |
|- F/ w ( x = z -> ph ) |
10 |
|
nfv |
|- F/ y x = z |
11 |
10 4
|
nfim |
|- F/ y ( x = z -> ps ) |
12 |
5
|
expcom |
|- ( y = w -> ( x = z -> ( ph <-> ps ) ) ) |
13 |
12
|
pm5.74d |
|- ( y = w -> ( ( x = z -> ph ) <-> ( x = z -> ps ) ) ) |
14 |
9 11 13
|
cbvalv1 |
|- ( A. y ( x = z -> ph ) <-> A. w ( x = z -> ps ) ) |
15 |
|
19.21v |
|- ( A. y ( x = z -> ph ) <-> ( x = z -> A. y ph ) ) |
16 |
|
19.21v |
|- ( A. w ( x = z -> ps ) <-> ( x = z -> A. w ps ) ) |
17 |
14 15 16
|
3bitr3i |
|- ( ( x = z -> A. y ph ) <-> ( x = z -> A. w ps ) ) |
18 |
17
|
pm5.74ri |
|- ( x = z -> ( A. y ph <-> A. w ps ) ) |
19 |
6 7 18
|
cbvalv1 |
|- ( A. x A. y ph <-> A. z A. w ps ) |