Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( ps /\ ph /\ ch ) -> ps ) |
2 |
1
|
a1i |
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> ps ) ) |
3 |
|
ax-5 |
|- ( ps -> A. x ps ) |
4 |
2 3
|
syl6 |
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ps ) ) |
5 |
|
simp2 |
|- ( ( ps /\ ph /\ ch ) -> ph ) |
6 |
5
|
imim1i |
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ph ) ) |
7 |
|
simp3 |
|- ( ( ps /\ ph /\ ch ) -> ch ) |
8 |
7
|
a1i |
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> ch ) ) |
9 |
|
ax-5 |
|- ( ch -> A. x ch ) |
10 |
8 9
|
syl6 |
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ch ) ) |
11 |
4 6 10
|
3jcad |
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> ( A. x ps /\ A. x ph /\ A. x ch ) ) ) |
12 |
|
19.26-3an |
|- ( A. x ( ps /\ ph /\ ch ) <-> ( A. x ps /\ A. x ph /\ A. x ch ) ) |
13 |
11 12
|
syl6ibr |
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) ) |