Step |
Hyp |
Ref |
Expression |
1 |
|
exancom |
|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) ) |
2 |
1
|
anbi1i |
|- ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) <-> ( E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) ) |
3 |
2
|
anbi2i |
|- ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) <-> ( E* x ps /\ ( E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) ) ) |
4 |
|
3anass |
|- ( ( E* x ps /\ E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) <-> ( E* x ps /\ ( E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) ) ) |
5 |
3 4
|
bitr4i |
|- ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) <-> ( E* x ps /\ E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) ) |
6 |
|
mopick2 |
|- ( ( E* x ps /\ E. x ( ps /\ ph ) /\ E. x ( ps /\ ch ) ) -> E. x ( ps /\ ph /\ ch ) ) |
7 |
5 6
|
sylbi |
|- ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) -> E. x ( ps /\ ph /\ ch ) ) |
8 |
|
3anass |
|- ( ( ps /\ ph /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) ) |
9 |
8
|
exbii |
|- ( E. x ( ps /\ ph /\ ch ) <-> E. x ( ps /\ ( ph /\ ch ) ) ) |
10 |
|
exsimpr |
|- ( E. x ( ps /\ ( ph /\ ch ) ) -> E. x ( ph /\ ch ) ) |
11 |
9 10
|
sylbi |
|- ( E. x ( ps /\ ph /\ ch ) -> E. x ( ph /\ ch ) ) |
12 |
7 11
|
syl |
|- ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) -> E. x ( ph /\ ch ) ) |
13 |
|
impexp |
|- ( ( ( E* x ps /\ ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) ) -> E. x ( ph /\ ch ) ) <-> ( E* x ps -> ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) -> E. x ( ph /\ ch ) ) ) ) |
14 |
12 13
|
mpbi |
|- ( E* x ps -> ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) -> E. x ( ph /\ ch ) ) ) |