Step |
Hyp |
Ref |
Expression |
1 |
|
ralimda.1 |
|- F/ x ph |
2 |
|
ralimda.2 |
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) ) |
3 |
|
nfra1 |
|- F/ x A. x e. A ps |
4 |
1 3
|
nfan |
|- F/ x ( ph /\ A. x e. A ps ) |
5 |
|
id |
|- ( ( ph /\ x e. A ) -> ( ph /\ x e. A ) ) |
6 |
5
|
adantlr |
|- ( ( ( ph /\ A. x e. A ps ) /\ x e. A ) -> ( ph /\ x e. A ) ) |
7 |
|
rspa |
|- ( ( A. x e. A ps /\ x e. A ) -> ps ) |
8 |
7
|
adantll |
|- ( ( ( ph /\ A. x e. A ps ) /\ x e. A ) -> ps ) |
9 |
6 8 2
|
sylc |
|- ( ( ( ph /\ A. x e. A ps ) /\ x e. A ) -> ch ) |
10 |
4 9
|
ralrimia |
|- ( ( ph /\ A. x e. A ps ) -> A. x e. A ch ) |
11 |
10
|
ex |
|- ( ph -> ( A. x e. A ps -> A. x e. A ch ) ) |