Step |
Hyp |
Ref |
Expression |
1 |
|
nfmo1 |
|- F/ x E* x ph |
2 |
|
nfe1 |
|- F/ x E. x ( ph /\ ps ) |
3 |
1 2
|
nfan |
|- F/ x ( E* x ph /\ E. x ( ph /\ ps ) ) |
4 |
|
mopick |
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) ) |
5 |
4
|
ancld |
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ( ph /\ ps ) ) ) |
6 |
5
|
anim1d |
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ( ph /\ ch ) -> ( ( ph /\ ps ) /\ ch ) ) ) |
7 |
|
df-3an |
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) ) |
8 |
6 7
|
syl6ibr |
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ( ph /\ ch ) -> ( ph /\ ps /\ ch ) ) ) |
9 |
3 8
|
eximd |
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( E. x ( ph /\ ch ) -> E. x ( ph /\ ps /\ ch ) ) ) |
10 |
9
|
3impia |
|- ( ( E* x ph /\ E. x ( ph /\ ps ) /\ E. x ( ph /\ ch ) ) -> E. x ( ph /\ ps /\ ch ) ) |