Step |
Hyp |
Ref |
Expression |
1 |
|
3anass |
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) ) |
2 |
1
|
2exbii |
|- ( E. y E. z ( ph /\ ps /\ ch ) <-> E. y E. z ( ph /\ ( ps /\ ch ) ) ) |
3 |
|
19.42vv |
|- ( E. y E. z ( ph /\ ( ps /\ ch ) ) <-> ( ph /\ E. y E. z ( ps /\ ch ) ) ) |
4 |
|
exdistr |
|- ( E. y E. z ( ps /\ ch ) <-> E. y ( ps /\ E. z ch ) ) |
5 |
4
|
anbi2i |
|- ( ( ph /\ E. y E. z ( ps /\ ch ) ) <-> ( ph /\ E. y ( ps /\ E. z ch ) ) ) |
6 |
2 3 5
|
3bitri |
|- ( E. y E. z ( ph /\ ps /\ ch ) <-> ( ph /\ E. y ( ps /\ E. z ch ) ) ) |
7 |
6
|
exbii |
|- ( E. x E. y E. z ( ph /\ ps /\ ch ) <-> E. x ( ph /\ E. y ( ps /\ E. z ch ) ) ) |