Step |
Hyp |
Ref |
Expression |
1 |
|
cgsex4g.1 |
|- ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) -> ch ) |
2 |
|
cgsex4g.2 |
|- ( ch -> ( ph <-> ps ) ) |
3 |
2
|
biimpa |
|- ( ( ch /\ ph ) -> ps ) |
4 |
3
|
exlimivv |
|- ( E. z E. w ( ch /\ ph ) -> ps ) |
5 |
4
|
exlimivv |
|- ( E. x E. y E. z E. w ( ch /\ ph ) -> ps ) |
6 |
|
elisset |
|- ( A e. R -> E. x x = A ) |
7 |
|
elisset |
|- ( B e. S -> E. y y = B ) |
8 |
6 7
|
anim12i |
|- ( ( A e. R /\ B e. S ) -> ( E. x x = A /\ E. y y = B ) ) |
9 |
|
elisset |
|- ( C e. R -> E. z z = C ) |
10 |
|
elisset |
|- ( D e. S -> E. w w = D ) |
11 |
9 10
|
anim12i |
|- ( ( C e. R /\ D e. S ) -> ( E. z z = C /\ E. w w = D ) ) |
12 |
8 11
|
anim12i |
|- ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> ( ( E. x x = A /\ E. y y = B ) /\ ( E. z z = C /\ E. w w = D ) ) ) |
13 |
|
19.42vv |
|- ( E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) <-> ( ( x = A /\ y = B ) /\ E. z E. w ( z = C /\ w = D ) ) ) |
14 |
13
|
2exbii |
|- ( E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) <-> E. x E. y ( ( x = A /\ y = B ) /\ E. z E. w ( z = C /\ w = D ) ) ) |
15 |
|
19.41vv |
|- ( E. x E. y ( ( x = A /\ y = B ) /\ E. z E. w ( z = C /\ w = D ) ) <-> ( E. x E. y ( x = A /\ y = B ) /\ E. z E. w ( z = C /\ w = D ) ) ) |
16 |
|
exdistrv |
|- ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) ) |
17 |
|
exdistrv |
|- ( E. z E. w ( z = C /\ w = D ) <-> ( E. z z = C /\ E. w w = D ) ) |
18 |
16 17
|
anbi12i |
|- ( ( E. x E. y ( x = A /\ y = B ) /\ E. z E. w ( z = C /\ w = D ) ) <-> ( ( E. x x = A /\ E. y y = B ) /\ ( E. z z = C /\ E. w w = D ) ) ) |
19 |
14 15 18
|
3bitri |
|- ( E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) <-> ( ( E. x x = A /\ E. y y = B ) /\ ( E. z z = C /\ E. w w = D ) ) ) |
20 |
12 19
|
sylibr |
|- ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) ) |
21 |
1
|
2eximi |
|- ( E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) -> E. z E. w ch ) |
22 |
21
|
2eximi |
|- ( E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) -> E. x E. y E. z E. w ch ) |
23 |
20 22
|
syl |
|- ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> E. x E. y E. z E. w ch ) |
24 |
2
|
biimprcd |
|- ( ps -> ( ch -> ph ) ) |
25 |
24
|
ancld |
|- ( ps -> ( ch -> ( ch /\ ph ) ) ) |
26 |
25
|
2eximdv |
|- ( ps -> ( E. z E. w ch -> E. z E. w ( ch /\ ph ) ) ) |
27 |
26
|
2eximdv |
|- ( ps -> ( E. x E. y E. z E. w ch -> E. x E. y E. z E. w ( ch /\ ph ) ) ) |
28 |
23 27
|
syl5com |
|- ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> ( ps -> E. x E. y E. z E. w ( ch /\ ph ) ) ) |
29 |
5 28
|
impbid2 |
|- ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> ( E. x E. y E. z E. w ( ch /\ ph ) <-> ps ) ) |